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

Theorem abbidv 2501
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 1626 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2500 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   {cab 2373
This theorem is referenced by:  cdeqab  3094  csbeq1  3197  sbcel12g  3209  sbceqg  3210  csbeq2d  3218  csbnestgf  3242  pweq  3745  sneq  3768  csbsng  3810  rabsn  3816  csbunig  3965  unieq  3966  inteq  3995  iineq1  4049  iineq2  4052  dfiin2g  4066  iinrab  4094  iinxprg  4109  opabbid  4211  csbxpg  4845  csbrng  5054  imasng  5166  iotaeq  5366  iotabi  5367  csbfv12gALT  5679  dfimafn  5714  fnsnfv  5725  fliftf  5976  oprabbid  6066  riotaeqdv  6486  recseq  6570  rdglim2  6626  qseq1  6890  qseq2  6891  qsinxp  6916  mapvalg  6964  ixpeq1  7009  fival  7352  cantnfreslem  7564  tcvalg  7610  karden  7752  acneq  7857  dfac2a  7943  infmap2  8031  cfval  8060  cflim3  8075  axdclem  8332  axdc  8334  rankcf  8585  genpv  8809  hashbclem  11628  hashf1lem2  11632  hashf1  11633  hashfac  11634  shftlem  11810  shftfib  11814  vdwlem6  13281  eqglact  14918  isghm  14933  symgval  15021  sylow1lem2  15160  sylow3lem1  15188  efgval  15276  dmdprd  15486  aspval2  16332  ressmplbas2  16445  cssval  16832  tgval  16943  clsval2  17037  lpfval  17125  lpval  17126  ptval  17523  hauspwpwf1  17940  ptcmplem2  18005  snclseqg  18066  ustval  18153  itg2val  19487  limcfval  19626  plyval  19979  isusgra0  21243  nbgraf1olem5  21321  nb3graprlem1  21326  fargshiftfo  21473  avril1  21605  elghomlem1  21797  nmoofval  22111  nmooval  22112  nmoo0  22140  nmopval  23207  nmfnval  23227  rabbidva2  23830  iunrdx  23858  disjabrex  23868  disjabrexf  23869  dfimafnf  23886  curry2ima  23938  sigaval  24289  measval  24348  orvcval  24494  derangval  24632  dfrtrcl2  24927  dfrdg2  25176  dfrdg3  25177  altxpeq1  25532  altxpeq2  25533  bpolylem  25808  supadd  25948  itg2addnc  25959  areacirclem6  25987  islocfin  26067  sdclem2  26137  sdc  26139  ismtyval  26200  eldiophb  26506  eldioph  26507  diophrw  26508  eldioph2  26511  eldioph2b  26512  eldioph3  26515  diophin  26522  diophun  26523  diophrex  26525  rexrabdioph  26545  rmxypairf1o  26665  hbtlem1  26996  hbtlem7  26998  dropab1  27318  dropab2  27319  csbdmg  27650  dfaimafn  27698  bnj956  28485  bnj18eq1  28636  bnj1318  28732  lfl1dim  29236  ldual1dim  29281  glbconxN  29492  lineset  29852  pointsetN  29855  psubspset  29858  pmapglb2xN  29886  polval2N  30020  psubclsetN  30050  lautset  30196  pautsetN  30212  tendofset  30872  tendoset  30873  dva1dim  31099  dia1dim2  31177  dib1dim2  31283  diclspsn  31309  dih1dimatlem  31444  dihglb2  31457  mapdvalc  31744  mapdval4N  31747  hdmap1ffval  31911  hdmapffval  31944  hgmapffval  32003
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380
  Copyright terms: Public domain W3C validator