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

Theorem opelxp 5034
 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 5022 . 2
2 vex 3112 . . . . . . 7
3 vex 3112 . . . . . . 7
42, 3opth2 4730 . . . . . 6
5 eleq1 2529 . . . . . . 7
6 eleq1 2529 . . . . . . 7
75, 6bi2anan9 873 . . . . . 6
84, 7sylbi 195 . . . . 5
98biimprcd 225 . . . 4
109rexlimivv 2954 . . 3
11 eqid 2457 . . . 4
12 opeq1 4217 . . . . . 6
1312eqeq2d 2471 . . . . 5
14 opeq2 4218 . . . . . 6
1514eqeq2d 2471 . . . . 5
1613, 15rspc2ev 3221 . . . 4
1711, 16mp3an3 1313 . . 3
1810, 17impbii 188 . 2
191, 18bitri 249 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  E.wrex 2808  <.cop 4035  X.cxp 5002 This theorem is referenced by:  brxp  5035  opelxpi  5036  opelxp1  5037  opelxp2  5038  otel3xp  5040  opthprc  5052  elxp3  5055  opeliunxp  5056  bropaex12  5078  optocl  5081  xpsspwOLD  5122  xpiindi  5143  opelres  5284  restidsing  5335  codir  5392  qfto  5393  xpnz  5431  difxp  5436  xpdifid  5440  ssrnres  5450  dfco2  5511  relssdmrn  5533  ressn  5548  opelf  5752  oprab4  6368  resoprab  6398  oprssdm  6456  nssdmovg  6457  ndmovg  6458  elmpt2cl  6517  resiexg  6736  fo1stres  6824  fo2ndres  6825  el2xptp0  6844  dfoprab4  6857  opiota  6859  bropopvvv  6880  curry1  6892  curry2  6895  xporderlem  6911  fnwelem  6915  mpt2xopxprcov0  6964  mpt2curryd  7017  brecop  7423  brecop2  7424  eceqoveq  7435  xpdom2  7632  mapunen  7706  dfac5lem2  8526  iunfo  8935  ordpipq  9341  prsrlem1  9470  opelcn  9527  opelreal  9528  elreal2  9530  swrd00  12645  swrdcl  12646  swrd0  12658  fsumcom2  13589  fprodcom2  13788  phimullem  14309  imasvscafn  14934  homarcl2  15362  evlfcl  15491  clatl  15746  matplusgcell  18935  mdetrlin  19104  iscnp2  19740  txuni2  20066  txcls  20105  txcnpi  20109  txcnp  20121  txcnmpt  20125  txdis1cn  20136  txtube  20141  hausdiag  20146  txlm  20149  tx1stc  20151  txkgen  20153  txflf  20507  tmdcn2  20588  tgphaus  20615  qustgplem  20619  fmucndlem  20794  xmeterval  20935  metustexhalfOLD  21066  metustexhalf  21067  blval2  21078  metuel2  21082  bcthlem1  21763  ovolfcl  21878  ovoliunlem1  21913  ovolshftlem1  21920  mbfimaopnlem  22062  limccnp2  22296  cxpcn3  23122  fsumvma  23488  lgsquadlem1  23629  lgsquadlem2  23630  2wlkonot3v  24875  2spthonot3v  24876  2wlkonotv  24877  numclwlk1lem2f  25092  ofresid  27482  xppreima2  27488  f1od2  27547  qtophaus  27839  eulerpartlemgvv  28315  erdszelem10  28644  cvmlift2lem10  28757  cvmlift2lem12  28759  msubff  28890  elmpst  28896  mpstrcl  28901  elmpps  28933  dfso2  29183  txpss3v  29528  pprodss4v  29534  dfrdg4  29600  heiborlem3  30309  pellex  30771  fourierdlem42  31931  etransclem44  32061  ndmaovg  32269  aoprssdm  32287  ndmaovcl  32288  ndmaovrcl  32289  ndmaovcom  32290  ndmaovass  32291  ndmaovdistr  32292  brcic  32582  opeliun2xp  32922  bj-elid3  34601  bj-eldiag2  34607  dibopelvalN  36870  dibopelval2  36872  dib1dim  36892  dihopcl  36980  dih1  37013  dih1dimatlem  37056  hdmap1val  37526 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-opab 4511  df-xp 5010
 Copyright terms: Public domain W3C validator