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

Theorem opabbidv 4515
Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 15-May-1995.)
Hypothesis
Ref Expression
opabbidv.1
Assertion
Ref Expression
opabbidv
Distinct variable groups:   ,   ,

Proof of Theorem opabbidv
StepHypRef Expression
1 nfv 1707 . 2
2 nfv 1707 . 2
3 opabbidv.1 . 2
41, 2, 3opabbid 4514 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  {copab 4509
This theorem is referenced by:  opabbii  4516  csbopab  4784  csbopabgALT  4785  csbmpt12  4786  xpeq1  5018  xpeq2  5019  opabbi2dv  5157  csbcnvgALT  5192  resopab2  5327  mptcnv  5413  cores  5515  xpco  5552  dffn5  5918  f1oiso2  6248  f1ocnvd  6524  ofreq  6543  bropopvvv  6880  fnwelem  6915  sprmpt2d  6971  mpt2curryd  7017  wemapwe  8160  wemapweOLD  8161  shftfval  12903  2shfti  12913  prdsval  14852  pwsle  14889  sectffval  15145  sectfval  15146  isfunc  15233  isfull  15279  isfth  15283  ipoval  15784  eqgfval  16249  dvdsrval  17294  dvdsrpropd  17345  ltbval  18136  opsrval  18139  lmfval  19733  xkocnv  20315  tgphaus  20615  isphtpc  21494  bcthlem1  21763  bcth  21768  ulmval  22775  lgsquadlem3  23631  iscgrg  23904  legval  23971  ishlg  23986  perpln1  24087  perpln2  24088  isperp  24089  ishpg  24128  iscgra  24169  wlks  24519  wlkcompim  24526  wlkelwrd  24530  wlkon  24533  trls  24538  trlon  24542  pths  24568  spths  24569  pthon  24577  spthon  24584  clwlk  24753  clwlkcompim  24764  iseupa  24965  ajfval  25724  f1o3d  27471  f1od2  27547  inftmrel  27724  isinftm  27725  metidval  27869  faeval  28218  eulerpartlemgvv  28315  eulerpart  28321  afsval  28551  fnopabeqd  30210  dnwech  30994  aomclem8  31007  dfafn5a  32245  lcvfbr  34745  cmtfvalN  34935  cvrfval  34993  dicffval  36901  dicfval  36902  dicval  36903  xpcogend  37773
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-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-opab 4511
  Copyright terms: Public domain W3C validator