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

Theorem abbidv 2397
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 1605 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2396 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   {cab 2269
This theorem is referenced by:  cdeqab  2981  csbeq1  3084  sbcel12g  3096  sbceqg  3097  csbeq2d  3105  csbnestgf  3129  pweq  3628  sneq  3651  csbsng  3692  rabsn  3697  csbunig  3835  unieq  3836  inteq  3865  iineq1  3919  iineq2  3922  dfiin2g  3936  iinrab  3964  iinxprg  3979  opabbid  4081  csbxpg  4716  csbrng  4923  imasng  5035  iotaeq  5227  iotabi  5228  csbfv12gALT  5536  dfimafn  5571  fnsnfv  5582  fliftf  5814  oprabbid  5901  riotaeqdv  6305  recseq  6389  rdglim2  6445  qseq1  6709  qseq2  6710  qsinxp  6735  mapvalg  6782  ixpeq1  6827  fival  7166  cantnfreslem  7377  tcvalg  7423  karden  7565  acneq  7670  dfac2a  7756  infmap2  7844  cfval  7873  cflim3  7888  axdclem  8146  axdc  8148  rankcf  8399  genpv  8623  hashbclem  11390  hashf1lem2  11394  hashf1  11395  hashfac  11396  shftlem  11563  shftfib  11567  vdwlem6  13033  eqglact  14668  isghm  14683  symgval  14771  sylow1lem2  14910  sylow3lem1  14938  efgval  15026  dmdprd  15236  aspval2  16086  ressmplbas2  16199  cssval  16582  tgval  16693  clsval2  16787  lpfval  16870  lpval  16871  ptval  17265  hauspwpwf1  17682  ptcmplem2  17747  snclseqg  17798  itg2val  19083  limcfval  19222  plyval  19575  avril1  20836  elghomlem1  21028  nmoofval  21340  nmooval  21341  nmoo0  21369  nmopval  22436  nmfnval  22456  dfimafnf  23041  iunrdx  23161  curry2ima  23247  disjabrex  23359  disjabrexf  23360  sigaval  23471  measval  23529  orvcval  23658  derangval  23698  dfrtrcl2  24045  dfrdg2  24152  dfrdg3  24153  altxpeq1  24507  altxpeq2  24508  bpolylem  24783  areacirclem6  24930  ab2rexexg  25122  isoriso  25212  prodeq1  25306  prodeq2  25307  prodeq3ii  25308  sallnei  25529  qusp  25542  vtarsu  25886  indcls2  25996  iscola2  26092  islocfin  26296  sdclem2  26452  sdc  26454  ismtyval  26524  eldiophb  26836  eldioph  26837  diophrw  26838  eldioph2  26841  eldioph2b  26842  eldioph3  26845  diophin  26852  diophun  26853  diophrex  26855  rexrabdioph  26875  rmxypairf1o  26996  hbtlem1  27327  hbtlem7  27329  dropab1  27650  dropab2  27651  csbdmg  27980  dfaimafn  28027  isusgra0  28106  bnj956  28808  bnj18eq1  28959  bnj1318  29055  lfl1dim  29311  ldual1dim  29356  glbconxN  29567  lineset  29927  pointsetN  29930  psubspset  29933  pmapglb2xN  29961  polval2N  30095  psubclsetN  30125  lautset  30271  pautsetN  30287  tendofset  30947  tendoset  30948  dva1dim  31174  dia1dim2  31252  dib1dim2  31358  diclspsn  31384  dih1dimatlem  31519  dihglb2  31532  mapdvalc  31819  mapdval4N  31822  hdmap1ffval  31986  hdmapffval  32019  hgmapffval  32078
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276
  Copyright terms: Public domain W3C validator