Theorem opelxp 5658

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 5646	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3442	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3442	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5426	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2822	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2822	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 638	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3176	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2734	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4827	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2745	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4828	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2745	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3587	. . . 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 2113  ∃wrex 3058  ⟨cop 4584   × cxp 5620

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 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

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 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-opab 5159  df-xp 5628

This theorem is referenced by:  opelxpi  5659  opelxp1  5664  opelxp2  5665  otelxp  5666  otel3xp  5668  brxp  5671  opthprc  5686  elxp3  5688  opeliunxp  5689  opeliun2xp  5690  bropaex12  5713  optoclOLD  5717  xpsspw  5756  inxp  5778  xpiindi  5782  opelres  5942  restidsing  6010  codir  6075  qfto  6076  xpnz  6115  difxp  6120  xpdifid  6124  dfco2  6201  ressn  6241  opelf  6693  oprab4  7442  resoprab  7474  oprssdm  7537  nssdmovg  7538  ndmovg  7539  elmpocl  7597  fo1stres  7957  fo2ndres  7958  dfoprab4  7997  opiota  8001  bropopvvv  8030  bropfvvvvlem  8031  curry1  8044  xporderlem  8067  fnwelem  8071  frpoins3xpg  8080  xpord2lem  8082  xpord2pred  8085  xpord2indlem  8087  mpoxopxprcov0  8157  mpocurryd  8209  on2recsov  8594  naddcllem  8602  brecop  8745  brecop2  8746  eceqoveq  8757  xpdom2  8998  mapunen  9072  djuss  9830  djuunxp  9831  dfac5lem2  10032  iunfo  10447  ordpipq  10851  prsrlem1  10981  opelcn  11038  opelreal  11039  elreal2  11041  swrdnznd  14564  swrd00  14566  swrdcl  14567  swrd0  14580  pfx00  14596  pfx0  14597  fsumcom2  15695  fprodcom2  15905  phimullem  16704  imasvscafn  17456  homarcl2  17957  evlfcl  18143  clatl  18429  pzriprnglem4  21437  pzriprnglem9  21442  matplusgcell  22375  iscnp2  23181  txuni2  23507  txcls  23546  txcnpi  23550  txcnp  23562  txcnmpt  23566  txdis1cn  23577  txtube  23582  hausdiag  23587  txlm  23590  tx1stc  23592  txkgen  23594  txflf  23948  tmdcn2  24031  tgphaus  24059  qustgplem  24063  fmucndlem  24232  xmeterval  24374  metustexhalf  24498  blval2  24504  bcthlem1  25278  ovolfcl  25421  ovoliunlem1  25457  mbfimaopnlem  25610  limccnp2  25847  fsumvma  27178  lgsquadlem1  27345  lgsquadlem2  27346  norec2ov  27927  dmrab  32520  xppreima2  32678  aciunf1lem  32689  f1od2  32747  smatrcl  33902  smatlem  33903  qtophaus  33942  eulerpartlemgvv  34482  erdszelem10  35343  cvmlift2lem10  35455  cvmlift2lem12  35457  msubff  35673  elmpst  35679  mpstrcl  35684  elmpps  35716  dfso2  35898  fv1stcnv  35920  fv2ndcnv  35921  txpss3v  36019  dfrdg4  36094  bj-opelrelex  37288  bj-opelidres  37305  bj-elid6  37314  bj-eldiag2  37321  bj-inftyexpitaudisj  37349  curf  37738  curunc  37742  heiborlem3  37953  xrnss3v  38505  ecxrn2  38532  inxpxrn  38542  dibopelvalN  41342  dibopelval2  41344  dib1dim  41364  dihopcl  41452  dih1  41485  dih1dimatlem  41528  hdmap1val  41997  aks6d1c3  42316  pellex  43019  elnonrel  43768  mnringmulrcld  44411  fourierdlem42  46335  etransclem44  46464  ovn0lem  46751  ndmaovg  47372  aoprssdm  47390  ndmaovcl  47391  ndmaovrcl  47392  ndmaovcom  47393  ndmaovass  47394  ndmaovdistr  47395  sprsymrelfvlem  47678  sprsymrelfolem2  47681  prproropf1olem2  47692  opgpgvtx  48243  iinxp  49018  coxp  49020  joindm2  49155  meetdm2  49157  swapf2fval  49452  swapf1val  49454  fuco2el  49499