Theorem: HTPI.Set_prod_def (HTPILib/Chap8Part2.lean)

State before:
U V : Type
A : Set U
B : Set V
a : U
b : V
⊢ (a, b) ∈ A ×ₛ B ↔ a ∈ A ∧ b ∈ B
Tactic:
rfl
State after:
no goals