Theorem opelxp 5720

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 5708	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3483	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3483	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5484	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2828	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2828	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 638	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3200	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2736	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4872	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2747	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4873	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2747	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3634	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1451	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 209	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 275	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∃wrex 3069  ⟨cop 4631   × cxp 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-opab 5205  df-xp 5690

This theorem is referenced by:  opelxpi  5721  opelxp1  5726  opelxp2  5727  otelxp  5728  otel3xp  5730  brxp  5733  opthprc  5748  elxp3  5750  opeliunxp  5751  opeliun2xp  5752  bropaex12  5776  optocl  5779  xpsspw  5818  inxp  5841  xpiindi  5845  opelres  6002  restidsing  6070  codir  6139  qfto  6140  xpnz  6178  difxp  6183  xpdifid  6187  dfco2  6264  relssdmrnOLD  6288  ressn  6304  opelf  6768  oprab4  7520  resoprab  7552  oprssdm  7615  nssdmovg  7616  ndmovg  7617  elmpocl  7675  fo1stres  8041  fo2ndres  8042  dfoprab4  8081  opiota  8085  bropopvvv  8116  bropfvvvvlem  8117  curry1  8130  xporderlem  8153  fnwelem  8157  frpoins3xpg  8166  xpord2lem  8168  xpord2pred  8171  xpord2indlem  8173  mpoxopxprcov0  8243  mpocurryd  8295  on2recsov  8707  naddcllem  8715  brecop  8851  brecop2  8852  eceqoveq  8863  xpdom2  9108  mapunen  9187  djuss  9961  djuunxp  9962  dfac5lem2  10165  iunfo  10580  ordpipq  10983  prsrlem1  11113  opelcn  11170  opelreal  11171  elreal2  11173  swrdnznd  14681  swrd00  14683  swrdcl  14684  swrd0  14697  pfx00  14713  pfx0  14714  fsumcom2  15811  fprodcom2  16021  phimullem  16817  imasvscafn  17583  homarcl2  18081  evlfcl  18268  clatl  18554  pzriprnglem4  21496  pzriprnglem9  21501  matplusgcell  22440  iscnp2  23248  txuni2  23574  txcls  23613  txcnpi  23617  txcnp  23629  txcnmpt  23633  txdis1cn  23644  txtube  23649  hausdiag  23654  txlm  23657  tx1stc  23659  txkgen  23661  txflf  24015  tmdcn2  24098  tgphaus  24126  qustgplem  24130  fmucndlem  24301  xmeterval  24443  metustexhalf  24570  blval2  24576  bcthlem1  25359  ovolfcl  25502  ovoliunlem1  25538  mbfimaopnlem  25691  limccnp2  25928  fsumvma  27258  lgsquadlem1  27425  lgsquadlem2  27426  norec2ov  27991  dmrab  32517  xppreima2  32662  aciunf1lem  32673  f1od2  32733  smatrcl  33796  smatlem  33797  qtophaus  33836  eulerpartlemgvv  34379  erdszelem10  35206  cvmlift2lem10  35318  cvmlift2lem12  35320  msubff  35536  elmpst  35542  mpstrcl  35547  elmpps  35579  dfso2  35756  fv1stcnv  35778  fv2ndcnv  35779  txpss3v  35880  dfrdg4  35953  bj-opelrelex  37146  bj-opelidres  37163  bj-elid6  37172  bj-eldiag2  37179  bj-inftyexpitaudisj  37207  curf  37606  curunc  37610  heiborlem3  37821  xrnss3v  38374  inxpxrn  38397  dibopelvalN  41146  dibopelval2  41148  dib1dim  41168  dihopcl  41256  dih1  41289  dih1dimatlem  41332  hdmap1val  41801  aks6d1c3  42125  pellex  42851  elnonrel  43603  mnringmulrcld  44252  fourierdlem42  46169  etransclem44  46298  ovn0lem  46585  ndmaovg  47201  aoprssdm  47219  ndmaovcl  47220  ndmaovrcl  47221  ndmaovcom  47222  ndmaovass  47223  ndmaovdistr  47224  sprsymrelfvlem  47482  sprsymrelfolem2  47485  prproropf1olem2  47496  opgpgvtx  48015  coxp  48749  joindm2  48872  meetdm2  48874  swapf2fval  48989  swapf1val  48991  fuco2el  49030