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

Theorem abbidv 2552
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 1630 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2551 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653   {cab 2424
This theorem is referenced by:  cdeqab  3153  csbeq1  3256  sbcel12g  3268  sbceqg  3269  csbeq2d  3277  csbnestgf  3301  pweq  3804  sneq  3827  csbsng  3869  rabsn  3875  csbunig  4025  unieq  4026  inteq  4055  iineq1  4109  iineq2  4112  dfiin2g  4126  iinrab  4155  iinxprg  4171  opabbid  4273  csbxpg  4908  csbrng  5117  imasng  5229  iotaeq  5429  iotabi  5430  csbfv12gALT  5742  dfimafn  5778  fnsnfv  5789  fliftf  6040  oprabbid  6130  riotaeqdv  6553  recseq  6637  rdglim2  6693  qseq1  6957  qseq2  6958  qsinxp  6983  mapvalg  7031  ixpeq1  7076  fival  7420  cantnfreslem  7634  tcvalg  7680  karden  7824  acneq  7929  dfac2a  8015  infmap2  8103  cfval  8132  cflim3  8147  axdclem  8404  axdc  8406  rankcf  8657  genpv  8881  hashbclem  11706  hashf1lem2  11710  hashf1  11711  hashfac  11712  shftlem  11888  shftfib  11892  vdwlem6  13359  eqglact  14996  isghm  15011  symgval  15099  sylow1lem2  15238  sylow3lem1  15266  efgval  15354  dmdprd  15564  aspval2  16410  ressmplbas2  16523  cssval  16914  tgval  17025  clsval2  17119  lpfval  17207  lpval  17208  ptval  17607  hauspwpwf1  18024  ptcmplem2  18089  snclseqg  18150  ustval  18237  itg2val  19623  limcfval  19764  plyval  20117  isusgra0  21381  nbgraf1olem5  21460  nb3graprlem1  21465  fargshiftfo  21630  avril1  21762  elghomlem1  21954  nmoofval  22268  nmooval  22269  nmoo0  22297  nmopval  23364  nmfnval  23384  rabbidva2  23991  iunrdx  24019  disjabrex  24029  disjabrexf  24030  dfimafnf  24048  curry2ima  24102  pstmval  24295  pstmfval  24296  sigaval  24498  measval  24557  orvcval  24720  derangval  24858  dfrtrcl2  25153  dfrdg2  25428  dfrdg3  25429  wrecseq123  25537  altxpeq1  25823  altxpeq2  25824  supadd  26246  mblfinlem3  26257  cnambfre  26267  itg2addnc  26273  areacirclem5  26310  islocfin  26390  sdclem2  26460  sdc  26462  ismtyval  26523  eldiophb  26829  eldioph  26830  diophrw  26831  eldioph2  26834  eldioph2b  26835  eldioph3  26838  diophin  26845  diophun  26846  diophrex  26848  rexrabdioph  26868  rmxypairf1o  26988  hbtlem1  27318  hbtlem7  27320  dropab1  27640  dropab2  27641  csbdmg  27972  dfaimafn  28019  rnfdmpr  28101  csbwrdg  28200  cshwsiun  28320  wwlknprop  28368  bnj956  29221  bnj18eq1  29372  bnj1318  29468  lfl1dim  29993  ldual1dim  30038  glbconxN  30249  lineset  30609  pointsetN  30612  psubspset  30615  pmapglb2xN  30643  polval2N  30777  psubclsetN  30807  lautset  30953  pautsetN  30969  tendofset  31629  tendoset  31630  dva1dim  31856  dia1dim2  31934  dib1dim2  32040  diclspsn  32066  dih1dimatlem  32201  dihglb2  32214  mapdvalc  32501  mapdval4N  32504  hdmap1ffval  32668  hdmapffval  32701  hgmapffval  32760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431
  Copyright terms: Public domain W3C validator