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

Theorem abbidv 2549
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 1629 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2548 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   {cab 2421
This theorem is referenced by:  cdeqab  3143  csbeq1  3246  sbcel12g  3258  sbceqg  3259  csbeq2d  3267  csbnestgf  3291  pweq  3794  sneq  3817  csbsng  3859  rabsn  3865  csbunig  4015  unieq  4016  inteq  4045  iineq1  4099  iineq2  4102  dfiin2g  4116  iinrab  4145  iinxprg  4160  opabbid  4262  csbxpg  4897  csbrng  5106  imasng  5218  iotaeq  5418  iotabi  5419  csbfv12gALT  5731  dfimafn  5767  fnsnfv  5778  fliftf  6029  oprabbid  6119  riotaeqdv  6542  recseq  6626  rdglim2  6682  qseq1  6946  qseq2  6947  qsinxp  6972  mapvalg  7020  ixpeq1  7065  fival  7409  cantnfreslem  7623  tcvalg  7669  karden  7811  acneq  7916  dfac2a  8002  infmap2  8090  cfval  8119  cflim3  8134  axdclem  8391  axdc  8393  rankcf  8644  genpv  8868  hashbclem  11693  hashf1lem2  11697  hashf1  11698  hashfac  11699  shftlem  11875  shftfib  11879  vdwlem6  13346  eqglact  14983  isghm  14998  symgval  15086  sylow1lem2  15225  sylow3lem1  15253  efgval  15341  dmdprd  15551  aspval2  16397  ressmplbas2  16510  cssval  16901  tgval  17012  clsval2  17106  lpfval  17194  lpval  17195  ptval  17594  hauspwpwf1  18011  ptcmplem2  18076  snclseqg  18137  ustval  18224  itg2val  19612  limcfval  19751  plyval  20104  isusgra0  21368  nbgraf1olem5  21447  nb3graprlem1  21452  fargshiftfo  21617  avril1  21749  elghomlem1  21941  nmoofval  22255  nmooval  22256  nmoo0  22284  nmopval  23351  nmfnval  23371  rabbidva2  23978  iunrdx  24006  disjabrex  24016  disjabrexf  24017  dfimafnf  24035  curry2ima  24089  pstmval  24282  pstmfval  24283  sigaval  24485  measval  24544  orvcval  24707  derangval  24845  dfrtrcl2  25140  dfrdg2  25415  dfrdg3  25416  wrecseq123  25524  altxpeq1  25810  altxpeq2  25811  supadd  26229  mblfinlem2  26235  cnambfre  26245  itg2addnc  26249  areacirclem6  26287  islocfin  26367  sdclem2  26437  sdc  26439  ismtyval  26500  eldiophb  26806  eldioph  26807  diophrw  26808  eldioph2  26811  eldioph2b  26812  eldioph3  26815  diophin  26822  diophun  26823  diophrex  26825  rexrabdioph  26845  rmxypairf1o  26965  hbtlem1  27295  hbtlem7  27297  dropab1  27617  dropab2  27618  csbdmg  27949  dfaimafn  27996  rnfdmpr  28069  cshwsiun  28249  bnj956  29084  bnj18eq1  29235  bnj1318  29331  lfl1dim  29856  ldual1dim  29901  glbconxN  30112  lineset  30472  pointsetN  30475  psubspset  30478  pmapglb2xN  30506  polval2N  30640  psubclsetN  30670  lautset  30816  pautsetN  30832  tendofset  31492  tendoset  31493  dva1dim  31719  dia1dim2  31797  dib1dim2  31903  diclspsn  31929  dih1dimatlem  32064  dihglb2  32077  mapdvalc  32364  mapdval4N  32367  hdmap1ffval  32531  hdmapffval  32564  hgmapffval  32623
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428
  Copyright terms: Public domain W3C validator