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

Theorem abbidv 2569
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 1761 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2568 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1444   {cab 2437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447
This theorem is referenced by:  rabbidva2  3034  cdeqab  3257  sbceqbid  3274  csbeq1  3366  csbeq2  3367  csbprc  3770  sbcel12  3772  sbceqg  3773  csbeq2d  3780  csbnestgf  3785  pweq  3954  sneq  3978  csbsng  4030  rabsn  4039  unieq  4206  csbuni  4226  inteq  4237  iineq1  4293  iineq2  4296  dfiin2g  4311  iinrab  4340  iinxprg  4359  opabbid  4465  imasng  5190  iotaeq  5554  iotabi  5555  dfimafn  5914  fnsnfv  5925  fliftf  6208  oprabbid  6344  wrecseq123  7029  rdglim2  7150  qseq1  7413  qseq2  7414  qsinxp  7439  mapvalg  7482  ixpsnval  7525  ixpeq1  7533  fival  7926  tcvalg  8222  karden  8366  acneq  8474  infmap2  8648  cfval  8677  cflim3  8692  axdclem  8949  axdc  8951  rankcf  9202  genpv  9424  negfi  10554  supadd  10575  hashf1lem2  12619  hashf1  12620  hashfac  12621  csbwrdg  12696  cleq1  13047  dfrtrcl2  13125  shftlem  13131  shftfib  13135  vdwlem6  14936  cshwsiun  15070  lubfval  16224  glbfval  16237  eqglact  16868  isghm  16883  symgval  17020  sylow1lem2  17251  sylow3lem1  17279  efgval  17367  dmdprd  17630  ixpsnbasval  18432  aspval2  18571  ressmplbas2  18679  cssval  19245  tgval  19970  clsval2  20065  lpfval  20154  lpval  20155  islocfin  20532  ptval  20585  hauspwpwf1  21002  ptcmplem2  21068  snclseqg  21130  ustval  21217  itg2val  22686  limcfval  22827  plyval  23147  isismt  24579  nbgraf1olem5  25173  nb3graprlem1  25179  fargshiftfo  25366  wwlknprop  25414  wwlknfi  25466  eclclwwlkn1  25560  rusgranumwlkb0  25681  rusgra0edg  25683  avril1  25900  elghomlem1OLD  26089  nmoofval  26403  nmooval  26404  nmoo0  26432  nmopval  27509  nmfnval  27529  iunrdx  28179  disjabrex  28192  disjabrexf  28193  dfimafnf  28233  curry2ima  28289  pstmval  28698  pstmfval  28699  sigaval  28932  measval  29020  orvcval  29290  bnj956  29588  bnj18eq1  29738  bnj1318  29834  derangval  29890  mclsval  30201  dfrdg2  30442  dfrdg3  30443  altxpeq1  30740  altxpeq2  30741  bj-snsetex  31557  bj-sngleq  31561  bj-projeq  31586  bj-projval  31590  csbwrecsg  31728  csboprabg  31731  finxpeq1  31778  finxpeq2  31779  csbfinxpg  31780  finxpreclem6  31788  ptrest  31939  poimirlem26  31966  poimirlem27  31967  poimirlem28  31968  mblfinlem3  31979  cnambfre  31989  itg2addnc  31996  areacirclem5  32036  sdclem2  32071  sdc  32073  ismtyval  32132  iineq12f  32408  lfl1dim  32687  ldual1dim  32732  glbconxN  32943  lineset  33303  pointsetN  33306  psubspset  33309  pmapglb2xN  33337  polval2N  33471  psubclsetN  33501  lautset  33647  pautsetN  33663  tendofset  34325  tendoset  34326  dva1dim  34552  dia1dim2  34630  dib1dim2  34736  diclspsn  34762  dih1dimatlem  34897  dihglb2  34910  hdmap1ffval  35364  hdmapffval  35397  hgmapffval  35456  eldiophb  35599  eldioph  35600  diophrw  35601  eldioph2  35604  eldioph2b  35605  eldioph3  35608  diophin  35615  diophun  35616  diophrex  35618  rexrabdioph  35637  rmxypairf1o  35759  hbtlem1  35982  hbtlem7  35984  nzss  36666  dropab1  36800  dropab2  36801  sbcel12gOLD  36905  csbunigOLD  37212  csbfv12gALTOLD  37213  csbxpgOLD  37214  csbrngOLD  37217  supsubc  37576  dfaimafn  38667  rnfdmpr  39015  nb3grprlem1  39454  vtxduhgrun  39538  rgrx0ndm  39608  ewlksfval  39618
  Copyright terms: Public domain W3C validator