Theorem opelxp 4779

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 4767	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 2816	. . . . . . 7 |- x e. _V
3		vex 2816	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4356	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2295	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2295	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 610	. . . . . 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 2666	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2232	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 3883	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2244	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 3884	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2244	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 2936	. . . 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 1363	. . 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 1398   e. wcel 2203   E.wrex 2521   <.cop 3692   X. cxp 4747

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-opab 4172  df-xp 4755

This theorem is referenced by:  brxp  4780  opelxpi  4781  opelxp1  4783  opelxp2  4784  opthprc  4801  elxp3  4804  opeliunxp  4805  optocl  4826  xpiindim  4892  opelres  5043  resiexg  5083  restidsing  5094  codir  5151  qfto  5152  xpmlem  5183  rnxpid  5197  ssrnres  5205  dfco2  5262  relssdmrn  5283  ressn  5303  opelf  5535  fnovex  6083  oprab4  6124  resoprab  6149  elmpocl  6249  fo1stresm  6355  fo2ndresm  6356  dfoprab4  6386  xporderlem  6427  f1od2  6431  brecop  6859  xpdom2  7082  mapunen  7104  djulclb  7346  djuss  7361  enq0enq  7746  enq0sym  7747  enq0tr  7749  nqnq0pi  7753  nnnq0lem1  7761  elinp  7789  genipv  7824  prsrlem1  8057  gt0srpr  8063  opelcn  8141  opelreal  8142  elreal2  8145  frecuzrdgrrn  10770  frec2uzrdg  10771  frecuzrdgrcl  10772  frecuzrdgsuc  10776  frecuzrdgrclt  10777  frecuzrdgsuctlem  10785  fisumcom2  12124  fprodcom2fi  12312  sqpweven  12872  2sqpwodd  12873  phimullem  12922  relelbasov  13275  txuni2  15121  txcnp  15136  txcnmpt  15138  txdis1cn  15143  txlm  15144  xmeterval  15300  limccnp2lem  15541  limccnp2cntop  15542  lgsquadlem1  15950  lgsquadlem2  15951