Theorem opelxp 5699

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 5687	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3461	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3461	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5464	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2853	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2853	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 650	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 220	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 253	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3209	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2765	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4840	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2776	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4841	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2776	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3596	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1479	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 212	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 278	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∃wrex 3091  ⟨cop 4597   × cxp 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5176  df-xp 5669

This theorem is used by:  opelxpi  5700  opelxp1  5705  opelxp2  5706  otelxp  5707  otel3xp  5709  brxp  5712  opthprc  5727  elxp3  5729  opeliunxp  5730  opeliun2xp  5731  bropaex12  5754  optoclOLD  5758  xpsspw  5798  inxp  5820  xpiindi  5823  opelres  5986  restidsing  6057  codir  6122  qfto  6123  xpnz  6158  difxp  6163  xpdifid  6167  xpdifcnvepel  6168  dfco2  6248  ressn  6290  opelf  6743  oprab4  7505  resoprab  7537  oprssdm  7601  nssdmovg  7602  ndmovg  7603  elmpocl  7661  fo1stres  8018  fo2ndres  8019  dfoprab4  8058  opiota  8062  bropopvvv  8091  bropfvvvvlem  8092  curry1  8105  xporderlem  8129  fnwelem  8133  frpoins3xpg  8142  xpord2lem  8144  xpord2pred  8147  xpord2indlem  8149  mpoxopxprcov0  8219  mpocurryd  8271  on2recsov  8660  naddcllem  8668  brecop  8814  brecop2  8815  eceqoveq  8826  xpdom2  9067  mapunen  9141  djuss  9922  djuunxp  9923  dfac5lem2  10124  iunfo  10540  ordpipq  10944  prsrlem1  11074  opelcn  11131  opelreal  11132  elreal2  11134  swrdnznd  14702  swrd00  14704  swrdcl  14705  swrd0  14720  pfx00  14736  pfx0  14737  fsumcom2  15850  fprodcom2  16063  phimullem  16862  imasvscafn  17615  homarcl2  18116  evlfcl  18302  clatl  18588  pzriprnglem4  21686  pzriprnglem9  21691  matplusgcell  22642  iscnp2  23448  txuni2  23775  txcls  23814  txcnpi  23818  txcnp  23830  txcnmpt  23834  txdis1cn  23845  txtube  23850  hausdiag  23855  txlm  23858  tx1stc  23860  txkgen  23862  txflf  24216  tmdcn2  24299  tgphaus  24327  qustgplem  24331  fmucndlem  24500  xmeterval  24642  metustexhalf  24766  blval2  24772  bcthlem1  25536  ovolfcl  25678  ovoliunlem1  25714  mbfimaopnlem  25867  limccnp2  26104  fsumvma  27430  lgsquadlem1  27597  lgsquadlem2  27598  norec2ov  28203  dmrab  32916  xppreima2  33069  aciunf1lem  33080  f1od2  33136  smatrcl  34252  smatlem  34253  qtophaus  34292  eulerpartlemgvv  34833  erdszelem10  35731  cvmlift2lem10  35843  cvmlift2lem12  35845  msubff  36061  elmpst  36067  mpstrcl  36072  elmpps  36104  dfso2  36286  fv1stcnv  36308  fv2ndcnv  36309  txpss3v  36407  dfrdg4  36482  bj-opelrelex  37847  bj-opelidres  37864  bj-elid6  37873  bj-eldiag2  37880  bj-inftyexpitaudisj  37908  curf  38308  curunc  38312  heiborlem3  38524  xrnss3v  39090  ecxrn2  39117  inxpxrn  39127  dibopelvalN  41977  dibopelval2  41979  dib1dim  41999  dihopcl  42087  dih1  42120  dih1dimatlem  42163  hdmap1val  42632  aks6d1c3  42950  pellex  43622  elnonrel  44371  mnringmulrcld  45012  fourierdlem42  46923  etransclem44  47052  ovn0lem  47339  ndmaovg  47981  aoprssdm  47999  ndmaovcl  48000  ndmaovrcl  48001  ndmaovcom  48002  ndmaovass  48003  ndmaovdistr  48004  sprsymrelfvlem  48299  sprsymrelfolem2  48302  prproropf1olem2  48313  opgpgvtx  48880  iinxp  49668  coxp  49670  joindm2  49805  meetdm2  49807  swapf2fval  50102  swapf1val  50104  fuco2el  50149