Metamath Proof Explorer

Theorem altopelaltxp

Description: Alternate ordered pair membership in a Cartesian product. Note that, unlike opelxp , there is no sethood requirement here. (Contributed by Scott Fenton, 22-Mar-2012)

Ref Expression
Assertion altopelaltxp ⊢ X Y ∈ A ×× B ↔ X ∈ A ∧ Y ∈ B

Proof

Step Hyp Ref Expression
1 elaltxp ⊢ X Y ∈ A ×× B ↔ ∃ x ∈ A ∃ y ∈ B X Y = x y
2 reeanv ⊢ ∃ x ∈ A ∃ y ∈ B x = X ∧ y = Y ↔ ∃ x ∈ A x = X ∧ ∃ y ∈ B y = Y
3 eqcom ⊢ X Y = x y ↔ x y = X Y
4 vex ⊢ x ∈ V
5 vex ⊢ y ∈ V
6 4 5 altopth ⊢ x y = X Y ↔ x = X ∧ y = Y
7 3 6 bitri ⊢ X Y = x y ↔ x = X ∧ y = Y
8 7 2rexbii ⊢ ∃ x ∈ A ∃ y ∈ B X Y = x y ↔ ∃ x ∈ A ∃ y ∈ B x = X ∧ y = Y
9 risset ⊢ X ∈ A ↔ ∃ x ∈ A x = X
10 risset ⊢ Y ∈ B ↔ ∃ y ∈ B y = Y
11 9 10 anbi12i ⊢ X ∈ A ∧ Y ∈ B ↔ ∃ x ∈ A x = X ∧ ∃ y ∈ B y = Y
12 2 8 11 3bitr4i ⊢ ∃ x ∈ A ∃ y ∈ B X Y = x y ↔ X ∈ A ∧ Y ∈ B
13 1 12 bitri ⊢ X Y ∈ A ×× B ↔ X ∈ A ∧ Y ∈ B