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 >> e. ( A XX. B ) <-> ( X e. A /\ Y e. B ) )

Proof

Step Hyp Ref Expression
1 elaltxp 
 |-  ( << X , Y >> e. ( A XX. B ) <-> E. x e. A E. y e. B << X , Y >> = << x , y >> )
2 reeanv 
 |-  ( E. x e. A E. y e. B ( x = X /\ y = Y ) <-> ( E. x e. A x = X /\ E. y e. B y = Y ) )
3 eqcom 
 |-  ( << X , Y >> = << x , y >> <-> << x , y >> = << X , Y >> )
4 vex 
 |-  x e. _V
5 vex 
 |-  y e. _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 
 |-  ( E. x e. A E. y e. B << X , Y >> = << x , y >> <-> E. x e. A E. y e. B ( x = X /\ y = Y ) )
9 risset 
 |-  ( X e. A <-> E. x e. A x = X )
10 risset 
 |-  ( Y e. B <-> E. y e. B y = Y )
11 9 10 anbi12i 
 |-  ( ( X e. A /\ Y e. B ) <-> ( E. x e. A x = X /\ E. y e. B y = Y ) )
12 2 8 11 3bitr4i 
 |-  ( E. x e. A E. y e. B << X , Y >> = << x , y >> <-> ( X e. A /\ Y e. B ) )
13 1 12 bitri 
 |-  ( << X , Y >> e. ( A XX. B ) <-> ( X e. A /\ Y e. B ) )