Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  opelxp Structured version   Visualization version   GIF version

Theorem opelxp 5070
 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.
StepHypRef Expression
1 elxp2 5056 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2 vex 3176 . . . . . . 7 𝑥 ∈ V
3 vex 3176 . . . . . . 7 𝑦 ∈ V
42, 3opth2 4875 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥𝐵 = 𝑦))
5 eleq1 2676 . . . . . . 7 (𝐴 = 𝑥 → (𝐴𝐶𝑥𝐶))
6 eleq1 2676 . . . . . . 7 (𝐵 = 𝑦 → (𝐵𝐷𝑦𝐷))
75, 6bi2anan9 913 . . . . . 6 ((𝐴 = 𝑥𝐵 = 𝑦) → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
84, 7sylbi 206 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
98biimprcd 239 . . . 4 ((𝑥𝐶𝑦𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷)))
109rexlimivv 3018 . . 3 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷))
11 eqid 2610 . . . 4 𝐴, 𝐵⟩ = ⟨𝐴, 𝐵
12 opeq1 4340 . . . . . 6 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
1312eqeq2d 2620 . . . . 5 (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14 opeq2 4341 . . . . . 6 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
1514eqeq2d 2620 . . . . 5 (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
1613, 15rspc2ev 3295 . . . 4 ((𝐴𝐶𝐵𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1711, 16mp3an3 1405 . . 3 ((𝐴𝐶𝐵𝐷) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1810, 17impbii 198 . 2 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴𝐶𝐵𝐷))
191, 18bitri 263 1 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∃wrex 2897  ⟨cop 4131   × cxp 5036 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-opab 4644  df-xp 5044 This theorem is referenced by:  brxp  5071  opelxpi  5072  opelxp1  5074  opelxp2  5075  otel3xp  5077  opthprc  5089  elxp3  5092  opeliunxp  5093  bropaex12  5115  optocl  5118  xpsspw  5156  xpiindi  5179  opelres  5322  restidsing  5377  restidsingOLD  5378  codir  5435  qfto  5436  xpnz  5472  difxp  5477  xpdifid  5481  ssrnres  5491  dfco2  5551  relssdmrn  5573  ressn  5588  elsnxpOLD  5595  opelf  5978  oprab4  6624  resoprab  6654  oprssdm  6713  nssdmovg  6714  ndmovg  6715  elmpt2cl  6774  resiexg  6994  fo1stres  7083  fo2ndres  7084  el2xptp0  7103  dfoprab4  7116  opiota  7118  bropopvvv  7142  bropfvvvvlem  7143  curry1  7156  curry2  7159  xporderlem  7175  fnwelem  7179  mpt2xopxprcov0  7230  mpt2curryd  7282  brecop  7727  brecop2  7728  eceqoveq  7740  xpdom2  7940  mapunen  8014  dfac5lem2  8830  iunfo  9240  ordpipq  9643  prsrlem1  9772  opelcn  9829  opelreal  9830  elreal2  9832  swrd00  13270  swrdcl  13271  swrd0  13286  fsumcom2  14347  fsumcom2OLD  14348  fprodcom2  14553  fprodcom2OLD  14554  phimullem  15322  imasvscafn  16020  brcic  16281  homarcl2  16508  evlfcl  16685  clatl  16939  matplusgcell  20058  mdetrlin  20227  iscnp2  20853  txuni2  21178  txcls  21217  txcnpi  21221  txcnp  21233  txcnmpt  21237  txdis1cn  21248  txtube  21253  hausdiag  21258  txlm  21261  tx1stc  21263  txkgen  21265  txflf  21620  tmdcn2  21703  tgphaus  21730  qustgplem  21734  fmucndlem  21905  xmeterval  22047  metustexhalf  22171  blval2  22177  metuel2  22180  bcthlem1  22929  ovolfcl  23042  ovoliunlem1  23077  ovolshftlem1  23084  mbfimaopnlem  23228  limccnp2  23462  cxpcn3  24289  fsumvma  24738  lgsquadlem1  24905  lgsquadlem2  24906  2wlkonot3v  26402  2spthonot3v  26403  2wlkonotv  26404  numclwlk1lem2f  26619  ofresid  28824  xppreima2  28830  aciunf1lem  28844  f1od2  28887  smatrcl  29190  smatlem  29191  qtophaus  29231  eulerpartlemgvv  29765  erdszelem10  30436  cvmlift2lem10  30548  cvmlift2lem12  30550  msubff  30681  elmpst  30687  mpstrcl  30692  elmpps  30724  dfso2  30897  fv1stcnv  30925  fv2ndcnv  30926  txpss3v  31155  pprodss4v  31161  dfrdg4  31228  bj-elid3  32264  bj-eldiag2  32269  curf  32557  curunc  32561  heiborlem3  32782  dibopelvalN  35450  dibopelval2  35452  dib1dim  35472  dihopcl  35560  dih1  35593  dih1dimatlem  35636  hdmap1val  36106  pellex  36417  elnonrel  36910  fourierdlem42  39042  etransclem44  39171  ovn0lem  39455  ndmaovg  39913  aoprssdm  39931  ndmaovcl  39932  ndmaovrcl  39933  ndmaovcom  39934  ndmaovass  39935  ndmaovdistr  39936  pfx00  40247  pfx0  40248  opeliun2xp  41904
 Copyright terms: Public domain W3C validator