Theorem opelxp 5668

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 5656	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3446	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3446	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5436	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2825	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2825	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 639	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3180	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2737	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4831	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2748	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4832	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2748	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3591	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1453	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 209	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 275	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  ⟨cop 4588   × cxp 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163  df-xp 5638

This theorem is referenced by:  opelxpi  5669  opelxp1  5674  opelxp2  5675  otelxp  5676  otel3xp  5678  brxp  5681  opthprc  5696  elxp3  5698  opeliunxp  5699  opeliun2xp  5700  bropaex12  5723  optoclOLD  5727  xpsspw  5766  inxp  5788  xpiindi  5792  opelres  5952  restidsing  6020  codir  6085  qfto  6086  xpnz  6125  difxp  6130  xpdifid  6134  dfco2  6211  ressn  6251  opelf  6703  oprab4  7454  resoprab  7486  oprssdm  7549  nssdmovg  7550  ndmovg  7551  elmpocl  7609  fo1stres  7969  fo2ndres  7970  dfoprab4  8009  opiota  8013  bropopvvv  8042  bropfvvvvlem  8043  curry1  8056  xporderlem  8079  fnwelem  8083  frpoins3xpg  8092  xpord2lem  8094  xpord2pred  8097  xpord2indlem  8099  mpoxopxprcov0  8169  mpocurryd  8221  on2recsov  8606  naddcllem  8614  brecop  8759  brecop2  8760  eceqoveq  8771  xpdom2  9012  mapunen  9086  djuss  9844  djuunxp  9845  dfac5lem2  10046  iunfo  10461  ordpipq  10865  prsrlem1  10995  opelcn  11052  opelreal  11053  elreal2  11055  swrdnznd  14578  swrd00  14580  swrdcl  14581  swrd0  14594  pfx00  14610  pfx0  14611  fsumcom2  15709  fprodcom2  15919  phimullem  16718  imasvscafn  17470  homarcl2  17971  evlfcl  18157  clatl  18443  pzriprnglem4  21451  pzriprnglem9  21456  matplusgcell  22389  iscnp2  23195  txuni2  23521  txcls  23560  txcnpi  23564  txcnp  23576  txcnmpt  23580  txdis1cn  23591  txtube  23596  hausdiag  23601  txlm  23604  tx1stc  23606  txkgen  23608  txflf  23962  tmdcn2  24045  tgphaus  24073  qustgplem  24077  fmucndlem  24246  xmeterval  24388  metustexhalf  24512  blval2  24518  bcthlem1  25292  ovolfcl  25435  ovoliunlem1  25471  mbfimaopnlem  25624  limccnp2  25861  fsumvma  27192  lgsquadlem1  27359  lgsquadlem2  27360  norec2ov  27965  dmrab  32583  xppreima2  32741  aciunf1lem  32752  f1od2  32809  smatrcl  33974  smatlem  33975  qtophaus  34014  eulerpartlemgvv  34554  erdszelem10  35416  cvmlift2lem10  35528  cvmlift2lem12  35530  msubff  35746  elmpst  35752  mpstrcl  35757  elmpps  35789  dfso2  35971  fv1stcnv  35993  fv2ndcnv  35994  txpss3v  36092  dfrdg4  36167  bj-opelrelex  37399  bj-opelidres  37416  bj-elid6  37425  bj-eldiag2  37432  bj-inftyexpitaudisj  37460  curf  37849  curunc  37853  heiborlem3  38064  xrnss3v  38632  ecxrn2  38659  inxpxrn  38669  dibopelvalN  41519  dibopelval2  41521  dib1dim  41541  dihopcl  41629  dih1  41662  dih1dimatlem  41705  hdmap1val  42174  aks6d1c3  42493  pellex  43192  elnonrel  43941  mnringmulrcld  44584  fourierdlem42  46507  etransclem44  46636  ovn0lem  46923  ndmaovg  47544  aoprssdm  47562  ndmaovcl  47563  ndmaovrcl  47564  ndmaovcom  47565  ndmaovass  47566  ndmaovdistr  47567  sprsymrelfvlem  47850  sprsymrelfolem2  47853  prproropf1olem2  47864  opgpgvtx  48415  iinxp  49190  coxp  49192  joindm2  49327  meetdm2  49329  swapf2fval  49624  swapf1val  49626  fuco2el  49671