Theorem opelxp 5021

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 5010	. 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 4718	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2532	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2532	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 869	. . . . . 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 2953	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2460	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 4206	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2474	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 4207	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2474	. . . . 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 1308	. . 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 1374   e. wcel 1762   E.wrex 2808   <.cop 4026   X. cxp 4990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-opab 4499  df-xp 4998

This theorem is referenced by:  brxp  5022  opelxpi  5023  opelxp1  5024  opelxp2  5025  otel3xp  5027  opthprc  5039  elxp3  5042  opeliunxp  5043  optocl  5067  xpsspwOLD  5108  xpiindi  5129  opelres  5270  restidsing  5321  codir  5378  qfto  5379  xpnz  5417  difxp  5422  xpdifid  5426  ssrnres  5436  dfco2  5497  relssdmrn  5519  ressn  5534  opelf  5738  oprab4  6343  resoprab  6373  oprssdm  6431  nssdmovg  6432  ndmovg  6433  elmpt2cl  6492  resiexg  6710  fo1stres  6798  fo2ndres  6799  el2xptp0  6818  dfoprab4  6831  opiota  6833  bropopvvv  6853  curry1  6865  curry2  6868  xporderlem  6884  fnwelem  6888  mpt2xopxprcov0  6935  mpt2curryd  6988  brecop  7394  brecop2  7395  eceqoveq  7406  xpdom2  7602  mapunen  7676  dfac5lem2  8494  iunfo  8903  ordpipq  9309  prsrlem1  9438  opelcn  9495  opelreal  9496  elreal2  9498  swrd00  12595  swrdcl  12596  swrd0  12608  fsumcom2  13538  phimullem  14157  imasvscafn  14781  homarcl2  15209  evlfcl  15338  clatl  15592  matplusgcell  18695  mdetrlin  18864  iscnp2  19499  txuni2  19794  txcls  19833  txcnpi  19837  txcnp  19849  txcnmpt  19853  txdis1cn  19864  txtube  19869  hausdiag  19874  txlm  19877  tx1stc  19879  txkgen  19881  txflf  20235  tmdcn2  20316  tgphaus  20343  divstgplem  20347  fmucndlem  20522  xmeterval  20663  metustexhalfOLD  20794  metustexhalf  20795  blval2  20806  metuel2  20810  bcthlem1  21491  ovolfcl  21606  ovoliunlem1  21641  ovolshftlem1  21648  mbfimaopnlem  21790  limccnp2  22024  cxpcn3  22843  fsumvma  23209  lgsquadlem1  23350  lgsquadlem2  23351  2wlkonot3v  24537  2spthonot3v  24538  2wlkonotv  24539  ofresid  27005  xppreima2  27010  f1od2  27069  qtophaus  27487  eulerpartlemgvv  27805  erdszelem10  28134  cvmlift2lem10  28247  cvmlift2lem12  28249  fprodcom2  28541  dfso2  28610  txpss3v  28955  pprodss4v  28961  dfrdg4  29027  heiborlem3  29763  pellex  30226  fourierdlem42  31268  ndmaovg  31555  aoprssdm  31573  ndmaovcl  31574  ndmaovrcl  31575  ndmaovcom  31576  ndmaovass  31577  ndmaovdistr  31578  numclwlk1lem2f  31811  opeliun2xp  31861  dibopelvalN  35815  dibopelval2  35817  dib1dim  35837  dihopcl  35925  dih1  35958  dih1dimatlem  36001  hdmap1val  36471