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

Theorem abbidv 2518
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 2517 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   {cab 2390
This theorem is referenced by:  cdeqab  3111  csbeq1  3214  sbcel12g  3226  sbceqg  3227  csbeq2d  3235  csbnestgf  3259  pweq  3762  sneq  3785  csbsng  3827  rabsn  3833  csbunig  3983  unieq  3984  inteq  4013  iineq1  4067  iineq2  4070  dfiin2g  4084  iinrab  4113  iinxprg  4128  opabbid  4230  csbxpg  4864  csbrng  5073  imasng  5185  iotaeq  5385  iotabi  5386  csbfv12gALT  5698  dfimafn  5734  fnsnfv  5745  fliftf  5996  oprabbid  6086  riotaeqdv  6509  recseq  6593  rdglim2  6649  qseq1  6913  qseq2  6914  qsinxp  6939  mapvalg  6987  ixpeq1  7032  fival  7375  cantnfreslem  7587  tcvalg  7633  karden  7775  acneq  7880  dfac2a  7966  infmap2  8054  cfval  8083  cflim3  8098  axdclem  8355  axdc  8357  rankcf  8608  genpv  8832  hashbclem  11656  hashf1lem2  11660  hashf1  11661  hashfac  11662  shftlem  11838  shftfib  11842  vdwlem6  13309  eqglact  14946  isghm  14961  symgval  15049  sylow1lem2  15188  sylow3lem1  15216  efgval  15304  dmdprd  15514  aspval2  16360  ressmplbas2  16473  cssval  16864  tgval  16975  clsval2  17069  lpfval  17157  lpval  17158  ptval  17555  hauspwpwf1  17972  ptcmplem2  18037  snclseqg  18098  ustval  18185  itg2val  19573  limcfval  19712  plyval  20065  isusgra0  21329  nbgraf1olem5  21408  nb3graprlem1  21413  fargshiftfo  21578  avril1  21710  elghomlem1  21902  nmoofval  22216  nmooval  22217  nmoo0  22245  nmopval  23312  nmfnval  23332  rabbidva2  23939  iunrdx  23967  disjabrex  23977  disjabrexf  23978  dfimafnf  23996  curry2ima  24050  pstmval  24243  pstmfval  24244  sigaval  24446  measval  24505  orvcval  24668  derangval  24806  dfrtrcl2  25101  dfrdg2  25366  dfrdg3  25367  altxpeq1  25722  altxpeq2  25723  bpolylem  25998  supadd  26138  mblfinlem2  26144  cnambfre  26154  itg2addnc  26158  areacirclem6  26186  islocfin  26266  sdclem2  26336  sdc  26338  ismtyval  26399  eldiophb  26705  eldioph  26706  diophrw  26707  eldioph2  26710  eldioph2b  26711  eldioph3  26714  diophin  26721  diophun  26722  diophrex  26724  rexrabdioph  26744  rmxypairf1o  26864  hbtlem1  27195  hbtlem7  27197  dropab1  27517  dropab2  27518  csbdmg  27849  dfaimafn  27896  rnfdmpr  27964  bnj956  28853  bnj18eq1  29004  bnj1318  29100  lfl1dim  29604  ldual1dim  29649  glbconxN  29860  lineset  30220  pointsetN  30223  psubspset  30226  pmapglb2xN  30254  polval2N  30388  psubclsetN  30418  lautset  30564  pautsetN  30580  tendofset  31240  tendoset  31241  dva1dim  31467  dia1dim2  31545  dib1dim2  31651  diclspsn  31677  dih1dimatlem  31812  dihglb2  31825  mapdvalc  32112  mapdval4N  32115  hdmap1ffval  32279  hdmapffval  32312  hgmapffval  32371
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397
  Copyright terms: Public domain W3C validator