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

Theorem abbidv 2565
Description: Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.)
Hypothesis
Ref Expression
abbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
abbidv  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem abbidv
StepHypRef Expression
1 nfv 1754 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2564 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   {cab 2414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424
This theorem is referenced by:  rabbidva2  3077  cdeqab  3295  sbceqbid  3312  csbeq1  3404  csbeq2  3405  csbprc  3804  sbcel12  3806  sbceqg  3807  csbeq2d  3814  csbnestgf  3819  pweq  3988  sneq  4012  csbsng  4061  rabsn  4070  unieq  4230  csbuni  4250  inteq  4261  iineq1  4317  iineq2  4320  dfiin2g  4335  iinrab  4364  iinxprg  4383  opabbid  4488  imasng  5210  iotaeq  5573  iotabi  5574  dfimafn  5930  fnsnfv  5941  fliftf  6223  oprabbid  6358  wrecseq123  7037  rdglim2  7158  qseq1  7421  qseq2  7422  qsinxp  7447  mapvalg  7490  ixpsnval  7533  ixpeq1  7541  fival  7932  tcvalg  8221  karden  8365  acneq  8472  infmap2  8646  cfval  8675  cflim3  8690  axdclem  8947  axdc  8949  rankcf  9201  genpv  9423  negfi  10554  supadd  10575  hashf1lem2  12614  hashf1  12615  hashfac  12616  csbwrdg  12683  cleq1  13026  dfrtrcl2  13104  shftlem  13110  shftfib  13114  vdwlem6  14899  cshwsiun  15033  lubfval  16175  glbfval  16188  eqglact  16819  isghm  16834  symgval  16971  sylow1lem2  17186  sylow3lem1  17214  efgval  17302  dmdprd  17565  ixpsnbasval  18367  aspval2  18506  ressmplbas2  18614  cssval  19176  tgval  19901  clsval2  19996  lpfval  20085  lpval  20086  islocfin  20463  ptval  20516  hauspwpwf1  20933  ptcmplem2  20999  snclseqg  21061  ustval  21148  itg2val  22563  limcfval  22704  plyval  23015  isismt  24439  nbgraf1olem5  25018  nb3graprlem1  25024  fargshiftfo  25211  wwlknprop  25259  wwlknfi  25311  eclclwwlkn1  25405  rusgranumwlkb0  25526  rusgra0edg  25528  avril1  25745  elghomlem1OLD  25934  nmoofval  26248  nmooval  26249  nmoo0  26277  nmopval  27344  nmfnval  27364  iunrdx  28018  disjabrex  28031  disjabrexf  28032  dfimafnf  28073  curry2ima  28129  pstmval  28537  pstmfval  28538  sigaval  28771  measval  28859  orvcval  29116  bnj956  29376  bnj18eq1  29526  bnj1318  29622  derangval  29678  mclsval  29989  dfrdg2  30229  dfrdg3  30230  altxpeq1  30525  altxpeq2  30526  bj-snsetex  31306  bj-sngleq  31310  bj-projeq  31335  bj-projval  31339  ptrest  31642  poimirlem26  31669  poimirlem27  31670  poimirlem28  31671  mblfinlem3  31682  cnambfre  31692  itg2addnc  31699  areacirclem5  31739  sdclem2  31774  sdc  31776  ismtyval  31835  iineq12f  32111  lfl1dim  32395  ldual1dim  32440  glbconxN  32651  lineset  33011  pointsetN  33014  psubspset  33017  pmapglb2xN  33045  polval2N  33179  psubclsetN  33209  lautset  33355  pautsetN  33371  tendofset  34033  tendoset  34034  dva1dim  34260  dia1dim2  34338  dib1dim2  34444  diclspsn  34470  dih1dimatlem  34605  dihglb2  34618  hdmap1ffval  35072  hdmapffval  35105  hgmapffval  35164  eldiophb  35307  eldioph  35308  diophrw  35309  eldioph2  35312  eldioph2b  35313  eldioph3  35316  diophin  35323  diophun  35324  diophrex  35326  rexrabdioph  35345  rmxypairf1o  35464  hbtlem1  35687  hbtlem7  35689  nzss  36302  dropab1  36436  dropab2  36437  sbcel12gOLD  36541  csbunigOLD  36851  csbfv12gALTOLD  36852  csbxpgOLD  36853  csbrngOLD  36856  dfaimafn  38056  rnfdmpr  38384
  Copyright terms: Public domain W3C validator