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

Theorem abbidv 2547
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 1672 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2546 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362   {cab 2419
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426
This theorem is referenced by:  rabbidva2  2952  cdeqab  3165  csbeq1  3279  csbeq2  3280  csbprc  3661  sbcel12  3663  sbcel12gOLD  3664  sbceqg  3665  csbeq2d  3674  csbnestgf  3680  pweq  3851  sneq  3875  csbsng  3923  rabsn  3930  unieq  4087  csbuni  4107  csbunigOLD  4108  inteq  4119  iineq1  4173  iineq2  4176  dfiin2g  4191  iinrab  4220  iinxprg  4236  opabbid  4342  csbxpgOLD  4906  imasng  5179  csbrngOLD  5288  iotaeq  5377  iotabi  5378  dfimafn  5728  fnsnfv  5739  fliftf  5995  oprabbid  6128  extmptsuppeq  6702  recseq  6819  rdglim2  6874  qseq1  7138  qseq2  7139  qsinxp  7164  mapvalg  7212  ixpsnval  7254  ixpeq1  7262  fival  7650  tcvalg  7946  karden  8090  acneq  8201  dfac2a  8287  infmap2  8375  cfval  8404  cflim3  8419  axdclem  8676  axdc  8678  rankcf  8932  genpv  9156  hashbclem  12189  hashf1lem2  12193  hashf1  12194  hashfac  12195  csbwrdg  12241  wrdlenfi  12242  shftlem  12541  shftfib  12545  vdwlem6  14030  cshwsiun  14109  lubfval  15131  glbfval  15144  eqglact  15712  isghm  15727  symgval  15864  sylow1lem2  16078  sylow3lem1  16106  efgval  16194  dmdprd  16454  ixpsnbasval  17212  aspval2  17339  ressmplbas2  17468  cssval  17949  tgval  18402  clsval2  18496  lpfval  18584  lpval  18585  ptval  18985  hauspwpwf1  19402  ptcmplem2  19467  snclseqg  19528  ustval  19619  itg2val  21048  limcfval  21189  plyval  21546  isusgra0  23098  nbgraf1olem5  23177  nb3graprlem1  23182  fargshiftfo  23347  avril1  23479  elghomlem1  23671  nmoofval  23985  nmooval  23986  nmoo0  24014  nmopval  25083  nmfnval  25103  sbceqbid  25688  iunrdx  25738  disjabrex  25750  disjabrexf  25751  dfimafnf  25774  curry2ima  25827  pstmval  26176  pstmfval  26177  sigaval  26407  measval  26466  orvcval  26688  derangval  26903  dfrtrcl2  27197  dfrdg2  27456  dfrdg3  27457  wrecseq123  27565  altxpeq1  27851  altxpeq2  27852  supadd  28262  ptrest  28269  mblfinlem3  28274  cnambfre  28284  itg2addnc  28290  areacirclem5  28332  islocfin  28412  sdclem2  28482  sdc  28484  ismtyval  28543  iineq12f  28821  eldiophb  28940  eldioph  28941  diophrw  28942  eldioph2  28945  eldioph2b  28946  eldioph3  28949  diophin  28956  diophun  28957  diophrex  28959  rexrabdioph  28977  rmxypairf1o  29097  hbtlem1  29324  hbtlem7  29326  dropab1  29548  dropab2  29549  dfaimafn  29917  rnfdmpr  29995  wwlknprop  30166  wwlkextwrd  30206  wwlknfi  30216  eclclwwlkn1  30352  rusgranumwlkl1  30405  rusgranumwlklem3  30415  rusgranumwlkb0  30417  rusgra0edg  30419  numclwwlkovf2  30523  csbfv12gALTOLD  31259  bnj956  31472  bnj18eq1  31622  bnj1318  31718  bj-snsetex  32039  bj-sngleq  32043  bj-projeq  32068  bj-projval  32072  lfl1dim  32339  ldual1dim  32384  glbconxN  32595  lineset  32955  pointsetN  32958  psubspset  32961  pmapglb2xN  32989  polval2N  33123  psubclsetN  33153  lautset  33299  pautsetN  33315  tendofset  33975  tendoset  33976  dva1dim  34202  dia1dim2  34280  dib1dim2  34386  diclspsn  34412  dih1dimatlem  34547  dihglb2  34560  mapdvalc  34847  mapdval4N  34850  hdmap1ffval  35014  hdmapffval  35047  hgmapffval  35106
  Copyright terms: Public domain W3C validator