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

Theorem abbidv 2603
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 1683 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2602 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379   {cab 2452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462
This theorem is referenced by:  rabbidva2  3103  cdeqab  3321  sbceqbid  3338  csbeq1  3438  csbeq2  3439  csbprc  3821  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  csbeq2d  3834  csbnestgf  3840  pweq  4013  sneq  4037  csbsng  4086  rabsn  4094  unieq  4253  csbuni  4273  csbunigOLD  4274  inteq  4285  iineq1  4340  iineq2  4343  dfiin2g  4358  iinrab  4387  iinxprg  4403  opabbid  4509  csbxpgOLD  5082  imasng  5359  csbrngOLD  5469  iotaeq  5559  iotabi  5560  dfimafn  5916  fnsnfv  5927  fliftf  6201  oprabbid  6334  extmptsuppeq  6924  recseq  7043  rdglim2  7098  qseq1  7361  qseq2  7362  qsinxp  7387  mapvalg  7430  ixpsnval  7472  ixpeq1  7480  fival  7872  tcvalg  8169  karden  8313  acneq  8424  dfac2a  8510  infmap2  8598  cfval  8627  cflim3  8642  axdclem  8899  axdc  8901  rankcf  9155  genpv  9377  hashbclem  12467  hashf1lem2  12471  hashf1  12472  hashfac  12473  csbwrdg  12536  shftlem  12864  shftfib  12868  vdwlem6  14363  cshwsiun  14442  lubfval  15465  glbfval  15478  eqglact  16057  isghm  16072  symgval  16209  sylow1lem2  16425  sylow3lem1  16453  efgval  16541  dmdprd  16832  ixpsnbasval  17655  aspval2  17795  ressmplbas2  17916  cssval  18508  tgval  19251  clsval2  19345  lpfval  19433  lpval  19434  ptval  19834  hauspwpwf1  20251  ptcmplem2  20316  snclseqg  20377  ustval  20468  itg2val  21898  limcfval  22039  plyval  22353  isismt  23677  isusgra0  24051  nbgraf1olem5  24149  nb3graprlem1  24155  fargshiftfo  24342  wwlknprop  24390  wwlkextwrd  24432  wwlknfi  24442  eclclwwlkn1  24536  rusgranumwlkl1  24651  rusgranumwlklem3  24655  rusgranumwlkb0  24657  rusgra0edg  24659  numclwwlkovf2  24789  avril1  24875  elghomlem1  25067  nmoofval  25381  nmooval  25382  nmoo0  25410  nmopval  26479  nmfnval  26499  iunrdx  27132  disjabrex  27144  disjabrexf  27145  dfimafnf  27174  curry2ima  27226  pstmval  27538  pstmfval  27539  sigaval  27778  measval  27837  orvcval  28064  derangval  28279  dfrtrcl2  28574  dfrdg2  28833  dfrdg3  28834  wrecseq123  28942  altxpeq1  29228  altxpeq2  29229  supadd  29647  ptrest  29653  mblfinlem3  29658  cnambfre  29668  itg2addnc  29674  areacirclem5  29716  islocfin  29796  sdclem2  29866  sdc  29868  ismtyval  29927  iineq12f  30205  eldiophb  30322  eldioph  30323  diophrw  30324  eldioph2  30327  eldioph2b  30328  eldioph3  30331  diophin  30338  diophun  30339  diophrex  30341  rexrabdioph  30359  rmxypairf1o  30479  hbtlem1  30704  hbtlem7  30706  nzss  30850  dropab1  30962  dropab2  30963  dfaimafn  31745  rnfdmpr  31803  csbfv12gALTOLD  32719  bnj956  32932  bnj18eq1  33082  bnj1318  33178  bj-snsetex  33620  bj-sngleq  33624  bj-projeq  33649  bj-projval  33653  lfl1dim  33936  ldual1dim  33981  glbconxN  34192  lineset  34552  pointsetN  34555  psubspset  34558  pmapglb2xN  34586  polval2N  34720  psubclsetN  34750  lautset  34896  pautsetN  34912  tendofset  35572  tendoset  35573  dva1dim  35799  dia1dim2  35877  dib1dim2  35983  diclspsn  36009  dih1dimatlem  36144  dihglb2  36157  mapdvalc  36444  mapdval4N  36447  hdmap1ffval  36611  hdmapffval  36644  hgmapffval  36703
  Copyright terms: Public domain W3C validator