Theorem opelxp 5018

Description: Ordered pair membership in a Cartesian 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 5006	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 3109	. . . . . . 7 |- x e. _V
3		vex 3109	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4715	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2526	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2526	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 871	. . . . . 6 |- ( ( A = x /\ B = y ) -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
8	4, 7	sylbi 195	. . . . 5 |- ( <. A , B >. = <. x , y >. -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
9	8	biimprcd 225	. . . 4 |- ( ( x e. C /\ y e. D ) -> ( <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) ) )
10	9	rexlimivv 2951	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2454	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 4203	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2468	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 4204	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2468	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 3218	. . . 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 1311	. . 3 |- ( ( A e. C /\ B e. D ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
18	10, 17	impbii 188	. 2 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. <-> ( A e. C /\ B e. D ) )
19	1, 18	bitri 249	1 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )

Syntax hints:   <-> wb 184   /\ wa 367   = wceq 1398   e. wcel 1823   E.wrex 2805   <.cop 4022   X. cxp 4986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-opab 4498  df-xp 4994

This theorem is referenced by:  brxp  5019  opelxpi  5020  opelxp1  5021  opelxp2  5022  otel3xp  5024  opthprc  5036  elxp3  5039  opeliunxp  5040  bropaex12  5062  optocl  5065  xpsspwOLD  5105  xpiindi  5127  opelres  5267  restidsing  5318  codir  5375  qfto  5376  xpnz  5411  difxp  5416  xpdifid  5420  ssrnres  5430  dfco2  5489  relssdmrn  5511  ressn  5526  opelf  5729  oprab4  6341  resoprab  6371  oprssdm  6429  nssdmovg  6430  ndmovg  6431  elmpt2cl  6490  resiexg  6709  fo1stres  6797  fo2ndres  6798  el2xptp0  6817  dfoprab4  6830  opiota  6832  bropopvvv  6853  curry1  6865  curry2  6868  xporderlem  6884  fnwelem  6888  mpt2xopxprcov0  6937  mpt2curryd  6990  brecop  7396  brecop2  7397  eceqoveq  7408  xpdom2  7605  mapunen  7679  dfac5lem2  8496  iunfo  8905  ordpipq  9309  prsrlem1  9438  opelcn  9495  opelreal  9496  elreal2  9498  swrd00  12634  swrdcl  12635  swrd0  12650  fsumcom2  13671  fprodcom2  13870  phimullem  14393  imasvscafn  15026  brcic  15286  homarcl2  15513  evlfcl  15690  clatl  15945  matplusgcell  19102  mdetrlin  19271  iscnp2  19907  txuni2  20232  txcls  20271  txcnpi  20275  txcnp  20287  txcnmpt  20291  txdis1cn  20302  txtube  20307  hausdiag  20312  txlm  20315  tx1stc  20317  txkgen  20319  txflf  20673  tmdcn2  20754  tgphaus  20781  qustgplem  20785  fmucndlem  20960  xmeterval  21101  metustexhalfOLD  21232  metustexhalf  21233  blval2  21244  metuel2  21248  bcthlem1  21929  ovolfcl  22044  ovoliunlem1  22079  ovolshftlem1  22086  mbfimaopnlem  22228  limccnp2  22462  cxpcn3  23290  fsumvma  23686  lgsquadlem1  23827  lgsquadlem2  23828  2wlkonot3v  25077  2spthonot3v  25078  2wlkonotv  25079  numclwlk1lem2f  25294  elsnxp  27684  ofresid  27703  xppreima2  27709  aciunf1lem  27729  f1od2  27778  qtophaus  28074  esum2dlem  28321  eulerpartlemgvv  28579  erdszelem10  28908  cvmlift2lem10  29021  cvmlift2lem12  29023  msubff  29154  elmpst  29160  mpstrcl  29165  elmpps  29197  dfso2  29424  txpss3v  29756  pprodss4v  29762  dfrdg4  29828  heiborlem3  30549  pellex  31010  fourierdlem42  32170  etransclem44  32300  ndmaovg  32508  aoprssdm  32526  ndmaovcl  32527  ndmaovrcl  32528  ndmaovcom  32529  ndmaovass  32530  ndmaovdistr  32531  pfx00  32612  pfx0  32613  opeliun2xp  33176  bj-elid3  35002  bj-eldiag2  35008  dibopelvalN  37267  dibopelval2  37269  dib1dim  37289  dihopcl  37377  dih1  37410  dih1dimatlem  37453  hdmap1val  37923