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

Theorem abbidv 2563
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 1673 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2562 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369   {cab 2429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439
This theorem is referenced by:  rabbidva2  2983  cdeqab  3197  sbceqbid  3214  csbeq1  3312  csbeq2  3313  csbprc  3694  sbcel12  3696  sbcel12gOLD  3697  sbceqg  3698  csbeq2d  3707  csbnestgf  3713  pweq  3884  sneq  3908  csbsng  3956  rabsn  3963  unieq  4120  csbuni  4140  csbunigOLD  4141  inteq  4152  iineq1  4206  iineq2  4209  dfiin2g  4224  iinrab  4253  iinxprg  4269  opabbid  4375  csbxpgOLD  4940  imasng  5212  csbrngOLD  5321  iotaeq  5410  iotabi  5411  dfimafn  5761  fnsnfv  5772  fliftf  6029  oprabbid  6160  extmptsuppeq  6734  recseq  6854  rdglim2  6909  qseq1  7171  qseq2  7172  qsinxp  7197  mapvalg  7245  ixpsnval  7287  ixpeq1  7295  fival  7683  tcvalg  7979  karden  8123  acneq  8234  dfac2a  8320  infmap2  8408  cfval  8437  cflim3  8452  axdclem  8709  axdc  8711  rankcf  8965  genpv  9189  hashbclem  12226  hashf1lem2  12230  hashf1  12231  hashfac  12232  csbwrdg  12278  wrdlenfi  12279  shftlem  12578  shftfib  12582  vdwlem6  14068  cshwsiun  14147  lubfval  15169  glbfval  15182  eqglact  15753  isghm  15768  symgval  15905  sylow1lem2  16119  sylow3lem1  16147  efgval  16235  dmdprd  16502  ixpsnbasval  17312  aspval2  17439  ressmplbas2  17556  cssval  18129  tgval  18582  clsval2  18676  lpfval  18764  lpval  18765  ptval  19165  hauspwpwf1  19582  ptcmplem2  19647  snclseqg  19708  ustval  19799  itg2val  21228  limcfval  21369  plyval  21683  isusgra0  23297  nbgraf1olem5  23376  nb3graprlem1  23381  fargshiftfo  23546  avril1  23678  elghomlem1  23870  nmoofval  24184  nmooval  24185  nmoo0  24213  nmopval  25282  nmfnval  25302  iunrdx  25936  disjabrex  25948  disjabrexf  25949  dfimafnf  25972  curry2ima  26025  pstmval  26344  pstmfval  26345  sigaval  26575  measval  26634  orvcval  26862  derangval  27077  dfrtrcl2  27372  dfrdg2  27631  dfrdg3  27632  wrecseq123  27740  altxpeq1  28026  altxpeq2  28027  supadd  28444  ptrest  28451  mblfinlem3  28456  cnambfre  28466  itg2addnc  28472  areacirclem5  28514  islocfin  28594  sdclem2  28664  sdc  28666  ismtyval  28725  iineq12f  29003  eldiophb  29121  eldioph  29122  diophrw  29123  eldioph2  29126  eldioph2b  29127  eldioph3  29130  diophin  29137  diophun  29138  diophrex  29140  rexrabdioph  29158  rmxypairf1o  29278  hbtlem1  29505  hbtlem7  29507  dropab1  29729  dropab2  29730  dfaimafn  30097  rnfdmpr  30175  wwlknprop  30346  wwlkextwrd  30386  wwlknfi  30396  eclclwwlkn1  30532  rusgranumwlkl1  30585  rusgranumwlklem3  30595  rusgranumwlkb0  30597  rusgra0edg  30599  numclwwlkovf2  30703  csbfv12gALTOLD  31653  bnj956  31866  bnj18eq1  32016  bnj1318  32112  bj-snsetex  32552  bj-sngleq  32556  bj-projeq  32581  bj-projval  32585  lfl1dim  32862  ldual1dim  32907  glbconxN  33118  lineset  33478  pointsetN  33481  psubspset  33484  pmapglb2xN  33512  polval2N  33646  psubclsetN  33676  lautset  33822  pautsetN  33838  tendofset  34498  tendoset  34499  dva1dim  34725  dia1dim2  34803  dib1dim2  34909  diclspsn  34935  dih1dimatlem  35070  dihglb2  35083  mapdvalc  35370  mapdval4N  35373  hdmap1ffval  35537  hdmapffval  35570  hgmapffval  35629
  Copyright terms: Public domain W3C validator