Theorem opelxp 4706

Description: Ordered pair membership in a cross product. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
opelxp	|- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )

Proof of Theorem opelxp

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp2 4694	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 2775	. . . . . . 7 |- x e. _V
3		vex 2775	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4285	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2268	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2268	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 606	. . . . . 6 |- ( ( A = x /\ B = y ) -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
8	4, 7	sylbi 121	. . . . 5 |- ( <. A , B >. = <. x , y >. -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
9	8	biimprcd 160	. . . 4 |- ( ( x e. C /\ y e. D ) -> ( <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) ) )
10	9	rexlimivv 2629	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2205	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 3819	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2217	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 3820	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2217	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 2892	. . . 4 |- ( ( A e. C /\ B e. D /\ <. A , B >. = <. A , B >. ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
17	11, 16	mp3an3 1339	. . 3 |- ( ( A e. C /\ B e. D ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
18	10, 17	impbii 126	. 2 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. <-> ( A e. C /\ B e. D ) )
19	1, 18	bitri 184	1 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1373   e. wcel 2176   E.wrex 2485   <.cop 3636   X. cxp 4674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219  ax-pr 4254

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-opab 4107  df-xp 4682

This theorem is referenced by:  brxp  4707  opelxpi  4708  opelxp1  4710  opelxp2  4711  opthprc  4727  elxp3  4730  opeliunxp  4731  optocl  4752  xpiindim  4816  opelres  4965  resiexg  5005  restidsing  5016  codir  5072  qfto  5073  xpmlem  5104  rnxpid  5118  ssrnres  5126  dfco2  5183  relssdmrn  5204  ressn  5224  opelf  5449  fnovex  5979  oprab4  6018  resoprab  6043  elmpocl  6143  fo1stresm  6249  fo2ndresm  6250  dfoprab4  6280  xporderlem  6319  f1od2  6323  brecop  6714  xpdom2  6928  djulclb  7159  djuss  7174  enq0enq  7546  enq0sym  7547  enq0tr  7549  nqnq0pi  7553  nnnq0lem1  7561  elinp  7589  genipv  7624  prsrlem1  7857  gt0srpr  7863  opelcn  7941  opelreal  7942  elreal2  7945  frecuzrdgrrn  10555  frec2uzrdg  10556  frecuzrdgrcl  10557  frecuzrdgsuc  10561  frecuzrdgrclt  10562  frecuzrdgsuctlem  10570  fisumcom2  11782  fprodcom2fi  11970  sqpweven  12530  2sqpwodd  12531  phimullem  12580  relelbasov  12927  txuni2  14761  txcnp  14776  txcnmpt  14778  txdis1cn  14783  txlm  14784  xmeterval  14940  limccnp2lem  15181  limccnp2cntop  15182  lgsquadlem1  15587  lgsquadlem2  15588