Theorem opelxp 5667

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 5655	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3448	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3448	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5435	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2816	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2816	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 638	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3177	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2729	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4833	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2740	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4834	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2740	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3598	. . . 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 1540   ∈ wcel 2109  ∃wrex 3053  ⟨cop 4591   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-opab 5165  df-xp 5637

This theorem is referenced by:  opelxpi  5668  opelxp1  5673  opelxp2  5674  otelxp  5675  otel3xp  5677  brxp  5680  opthprc  5695  elxp3  5697  opeliunxp  5698  opeliun2xp  5699  bropaex12  5722  optocl  5725  xpsspw  5763  inxp  5785  xpiindi  5789  opelres  5945  restidsing  6013  codir  6081  qfto  6082  xpnz  6120  difxp  6125  xpdifid  6129  dfco2  6206  relssdmrnOLD  6230  ressn  6246  opelf  6703  oprab4  7455  resoprab  7487  oprssdm  7550  nssdmovg  7551  ndmovg  7552  elmpocl  7610  fo1stres  7973  fo2ndres  7974  dfoprab4  8013  opiota  8017  bropopvvv  8046  bropfvvvvlem  8047  curry1  8060  xporderlem  8083  fnwelem  8087  frpoins3xpg  8096  xpord2lem  8098  xpord2pred  8101  xpord2indlem  8103  mpoxopxprcov0  8173  mpocurryd  8225  on2recsov  8609  naddcllem  8617  brecop  8760  brecop2  8761  eceqoveq  8772  xpdom2  9013  mapunen  9087  djuss  9849  djuunxp  9850  dfac5lem2  10053  iunfo  10468  ordpipq  10871  prsrlem1  11001  opelcn  11058  opelreal  11059  elreal2  11061  swrdnznd  14583  swrd00  14585  swrdcl  14586  swrd0  14599  pfx00  14615  pfx0  14616  fsumcom2  15716  fprodcom2  15926  phimullem  16725  imasvscafn  17476  homarcl2  17973  evlfcl  18159  clatl  18443  pzriprnglem4  21370  pzriprnglem9  21375  matplusgcell  22296  iscnp2  23102  txuni2  23428  txcls  23467  txcnpi  23471  txcnp  23483  txcnmpt  23487  txdis1cn  23498  txtube  23503  hausdiag  23508  txlm  23511  tx1stc  23513  txkgen  23515  txflf  23869  tmdcn2  23952  tgphaus  23980  qustgplem  23984  fmucndlem  24154  xmeterval  24296  metustexhalf  24420  blval2  24426  bcthlem1  25200  ovolfcl  25343  ovoliunlem1  25379  mbfimaopnlem  25532  limccnp2  25769  fsumvma  27100  lgsquadlem1  27267  lgsquadlem2  27268  norec2ov  27840  dmrab  32399  xppreima2  32548  aciunf1lem  32559  f1od2  32617  smatrcl  33759  smatlem  33760  qtophaus  33799  eulerpartlemgvv  34340  erdszelem10  35160  cvmlift2lem10  35272  cvmlift2lem12  35274  msubff  35490  elmpst  35496  mpstrcl  35501  elmpps  35533  dfso2  35715  fv1stcnv  35737  fv2ndcnv  35738  txpss3v  35839  dfrdg4  35912  bj-opelrelex  37105  bj-opelidres  37122  bj-elid6  37131  bj-eldiag2  37138  bj-inftyexpitaudisj  37166  curf  37565  curunc  37569  heiborlem3  37780  xrnss3v  38327  inxpxrn  38354  dibopelvalN  41110  dibopelval2  41112  dib1dim  41132  dihopcl  41220  dih1  41253  dih1dimatlem  41296  hdmap1val  41765  aks6d1c3  42084  pellex  42796  elnonrel  43547  mnringmulrcld  44190  fourierdlem42  46120  etransclem44  46249  ovn0lem  46536  ndmaovg  47158  aoprssdm  47176  ndmaovcl  47177  ndmaovrcl  47178  ndmaovcom  47179  ndmaovass  47180  ndmaovdistr  47181  sprsymrelfvlem  47464  sprsymrelfolem2  47467  prproropf1olem2  47478  opgpgvtx  48019  iinxp  48792  coxp  48794  joindm2  48929  meetdm2  48931  swapf2fval  49227  swapf1val  49229  fuco2el  49274