Theorem opelxp 4864

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 4853	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 2970	. . . . . . 7 |- x e. _V
3		vex 2970	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4565	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2498	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2498	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 868	. . . . . 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 2841	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2438	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 4054	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2449	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 4055	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2449	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 3076	. . . 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 1303	. . 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 369   = wceq 1369   e. wcel 1756   E.wrex 2711   <.cop 3878   X. cxp 4833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-opab 4346  df-xp 4841

This theorem is referenced by:  brxp  4865  opelxpi  4866  opelxp1  4867  opelxp2  4868  opthprc  4881  elxp3  4884  opeliunxp  4885  optocl  4908  xpsspwOLD  4949  xpiindi  4970  opelres  5111  restidsing  5157  codir  5213  qfto  5214  xpnz  5252  difxp  5257  xpdifid  5261  ssrnres  5271  dfco2  5332  relssdmrn  5353  ressn  5368  opelf  5569  oprab4  6152  resoprab  6181  oprssdm  6239  nssdmovg  6240  ndmovg  6241  elmpt2cl  6299  resiexg  6509  fo1stres  6595  fo2ndres  6596  dfoprab4  6626  opiota  6628  bropopvvv  6648  curry1  6659  curry2  6662  xporderlem  6678  fnwelem  6682  mpt2xopxprcov0  6729  brecop  7185  brecop2  7186  eceqoveq  7197  xpdom2  7398  mapunen  7472  dfac5lem2  8286  iunfo  8695  ordpipq  9103  opelcn  9288  opelreal  9289  elreal2  9291  swrd00  12306  swrdcl  12307  swrd0  12319  fsumcom2  13233  phimullem  13846  imasvscafn  14467  homarcl2  14895  evlfcl  15024  clatl  15278  mdetrlin  18389  iscnp2  18823  txuni2  19118  txcls  19157  txcnpi  19161  txcnp  19173  txcnmpt  19177  txdis1cn  19188  txtube  19193  hausdiag  19198  txlm  19201  tx1stc  19203  txkgen  19205  txflf  19559  tmdcn2  19640  tgphaus  19667  divstgplem  19671  fmucndlem  19846  xmeterval  19987  metustexhalfOLD  20118  metustexhalf  20119  blval2  20130  metuel2  20134  bcthlem1  20815  ovolfcl  20930  ovoliunlem1  20965  ovolshftlem1  20972  mbfimaopnlem  21113  limccnp2  21347  cxpcn3  22166  fsumvma  22532  lgsquadlem1  22673  lgsquadlem2  22674  ofresid  25928  xppreima2  25933  f1od2  25992  eulerpartlemgvv  26728  erdszelem10  27057  cvmlift2lem10  27170  cvmlift2lem12  27172  fprodcom2  27464  dfso2  27533  txpss3v  27878  pprodss4v  27884  dfrdg4  27950  heiborlem3  28683  pellex  29147  ndmaovg  30061  aoprssdm  30079  ndmaovcl  30080  ndmaovrcl  30081  ndmaovcom  30082  ndmaovass  30083  ndmaovdistr  30084  el2xptp0  30098  otel3xp  30099  2wlkonot3v  30365  2spthonot3v  30366  2wlkonotv  30367  numclwlk1lem2f  30656  opeliun2xp  30690  matplusgcell  30819  dibopelvalN  34681  dibopelval2  34683  dib1dim  34703  dihopcl  34791  dih1  34824  dih1dimatlem  34867  hdmap1val  35337