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

Theorem abbidv 2410
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 1609 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2409 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   {cab 2282
This theorem is referenced by:  cdeqab  2994  csbeq1  3097  sbcel12g  3109  sbceqg  3110  csbeq2d  3118  csbnestgf  3142  pweq  3641  sneq  3664  csbsng  3705  rabsn  3710  csbunig  3851  unieq  3852  inteq  3881  iineq1  3935  iineq2  3938  dfiin2g  3952  iinrab  3980  iinxprg  3995  opabbid  4097  csbxpg  4732  csbrng  4939  imasng  5051  iotaeq  5243  iotabi  5244  csbfv12gALT  5552  dfimafn  5587  fnsnfv  5598  fliftf  5830  oprabbid  5917  riotaeqdv  6321  recseq  6405  rdglim2  6461  qseq1  6725  qseq2  6726  qsinxp  6751  mapvalg  6798  ixpeq1  6843  fival  7182  cantnfreslem  7393  tcvalg  7439  karden  7581  acneq  7686  dfac2a  7772  infmap2  7860  cfval  7889  cflim3  7904  axdclem  8162  axdc  8164  rankcf  8415  genpv  8639  hashbclem  11406  hashf1lem2  11410  hashf1  11411  hashfac  11412  shftlem  11579  shftfib  11583  vdwlem6  13049  eqglact  14684  isghm  14699  symgval  14787  sylow1lem2  14926  sylow3lem1  14954  efgval  15042  dmdprd  15252  aspval2  16102  ressmplbas2  16215  cssval  16598  tgval  16709  clsval2  16803  lpfval  16886  lpval  16887  ptval  17281  hauspwpwf1  17698  ptcmplem2  17763  snclseqg  17814  itg2val  19099  limcfval  19238  plyval  19591  avril1  20852  elghomlem1  21044  nmoofval  21356  nmooval  21357  nmoo0  21385  nmopval  22452  nmfnval  22472  dfimafnf  23057  iunrdx  23177  curry2ima  23262  disjabrex  23374  disjabrexf  23375  sigaval  23486  measval  23544  orvcval  23673  derangval  23713  dfrtrcl2  24060  dfrdg2  24223  dfrdg3  24224  altxpeq1  24579  altxpeq2  24580  bpolylem  24855  supadd  24996  itg2addnc  25005  areacirclem6  25033  ab2rexexg  25225  isoriso  25315  prodeq1  25409  prodeq2  25410  prodeq3ii  25411  sallnei  25632  qusp  25645  vtarsu  25989  indcls2  26099  iscola2  26195  islocfin  26399  sdclem2  26555  sdc  26557  ismtyval  26627  eldiophb  26939  eldioph  26940  diophrw  26941  eldioph2  26944  eldioph2b  26945  eldioph3  26948  diophin  26955  diophun  26956  diophrex  26958  rexrabdioph  26978  rmxypairf1o  27099  hbtlem1  27430  hbtlem7  27432  dropab1  27753  dropab2  27754  csbdmg  28085  dfaimafn  28133  isusgra0  28238  nb3graprlem1  28287  fargshiftfo  28383  bnj956  29124  bnj18eq1  29275  bnj1318  29371  lfl1dim  29933  ldual1dim  29978  glbconxN  30189  lineset  30549  pointsetN  30552  psubspset  30555  pmapglb2xN  30583  polval2N  30717  psubclsetN  30747  lautset  30893  pautsetN  30909  tendofset  31569  tendoset  31570  dva1dim  31796  dia1dim2  31874  dib1dim2  31980  diclspsn  32006  dih1dimatlem  32141  dihglb2  32154  mapdvalc  32441  mapdval4N  32444  hdmap1ffval  32608  hdmapffval  32641  hgmapffval  32700
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289
  Copyright terms: Public domain W3C validator