Theorem opelxp 5650

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	⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Proof of Theorem opelxp

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp2 5638	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3440	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3440	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5418	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2819	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2819	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 638	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3174	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2731	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4822	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2742	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4823	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2742	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3585	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1452	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 209	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 275	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∃wrex 3056  ⟨cop 4579   × cxp 5612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-opab 5152  df-xp 5620

This theorem is referenced by:  opelxpi  5651  opelxp1  5656  opelxp2  5657  otelxp  5658  otel3xp  5660  brxp  5663  opthprc  5678  elxp3  5680  opeliunxp  5681  opeliun2xp  5682  bropaex12  5705  optoclOLD  5709  xpsspw  5748  inxp  5770  xpiindi  5774  opelres  5933  restidsing  6001  codir  6066  qfto  6067  xpnz  6106  difxp  6111  xpdifid  6115  dfco2  6192  ressn  6232  opelf  6684  oprab4  7432  resoprab  7464  oprssdm  7527  nssdmovg  7528  ndmovg  7529  elmpocl  7587  fo1stres  7947  fo2ndres  7948  dfoprab4  7987  opiota  7991  bropopvvv  8020  bropfvvvvlem  8021  curry1  8034  xporderlem  8057  fnwelem  8061  frpoins3xpg  8070  xpord2lem  8072  xpord2pred  8075  xpord2indlem  8077  mpoxopxprcov0  8147  mpocurryd  8199  on2recsov  8583  naddcllem  8591  brecop  8734  brecop2  8735  eceqoveq  8746  xpdom2  8985  mapunen  9059  djuss  9813  djuunxp  9814  dfac5lem2  10015  iunfo  10430  ordpipq  10833  prsrlem1  10963  opelcn  11020  opelreal  11021  elreal2  11023  swrdnznd  14550  swrd00  14552  swrdcl  14553  swrd0  14566  pfx00  14582  pfx0  14583  fsumcom2  15681  fprodcom2  15891  phimullem  16690  imasvscafn  17441  homarcl2  17942  evlfcl  18128  clatl  18414  pzriprnglem4  21421  pzriprnglem9  21426  matplusgcell  22348  iscnp2  23154  txuni2  23480  txcls  23519  txcnpi  23523  txcnp  23535  txcnmpt  23539  txdis1cn  23550  txtube  23555  hausdiag  23560  txlm  23563  tx1stc  23565  txkgen  23567  txflf  23921  tmdcn2  24004  tgphaus  24032  qustgplem  24036  fmucndlem  24205  xmeterval  24347  metustexhalf  24471  blval2  24477  bcthlem1  25251  ovolfcl  25394  ovoliunlem1  25430  mbfimaopnlem  25583  limccnp2  25820  fsumvma  27151  lgsquadlem1  27318  lgsquadlem2  27319  norec2ov  27900  dmrab  32476  xppreima2  32633  aciunf1lem  32644  f1od2  32702  smatrcl  33809  smatlem  33810  qtophaus  33849  eulerpartlemgvv  34389  erdszelem10  35244  cvmlift2lem10  35356  cvmlift2lem12  35358  msubff  35574  elmpst  35580  mpstrcl  35585  elmpps  35617  dfso2  35799  fv1stcnv  35821  fv2ndcnv  35822  txpss3v  35920  dfrdg4  35995  bj-opelrelex  37188  bj-opelidres  37205  bj-elid6  37214  bj-eldiag2  37221  bj-inftyexpitaudisj  37249  curf  37648  curunc  37652  heiborlem3  37863  xrnss3v  38415  ecxrn2  38442  inxpxrn  38452  dibopelvalN  41252  dibopelval2  41254  dib1dim  41274  dihopcl  41362  dih1  41395  dih1dimatlem  41438  hdmap1val  41907  aks6d1c3  42226  pellex  42938  elnonrel  43688  mnringmulrcld  44331  fourierdlem42  46257  etransclem44  46386  ovn0lem  46673  ndmaovg  47294  aoprssdm  47312  ndmaovcl  47313  ndmaovrcl  47314  ndmaovcom  47315  ndmaovass  47316  ndmaovdistr  47317  sprsymrelfvlem  47600  sprsymrelfolem2  47603  prproropf1olem2  47614  opgpgvtx  48165  iinxp  48941  coxp  48943  joindm2  49078  meetdm2  49080  swapf2fval  49376  swapf1val  49378  fuco2el  49423