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

Theorem rabeq 2959
Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.)
Assertion
Ref Expression
rabeq  |-  ( A  =  B  ->  { x  e.  A  |  ph }  =  { x  e.  B  |  ph } )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem rabeq
StepHypRef Expression
1 nfcv 2579 . 2  |-  F/_ x A
2 nfcv 2579 . 2  |-  F/_ x B
31, 2rabeqf 2958 1  |-  ( A  =  B  ->  { x  e.  A  |  ph }  =  { x  e.  B  |  ph } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1654   {crab 2716
This theorem is referenced by:  rabeqbidv  2960  rabeqbidva  2961  difeq1  3447  ifeq1  3771  ifeq2  3772  rabrsn  3903  pmvalg  7065  supeq2  7489  oieq2  7518  cantnffval  7654  scott0  7848  hsmex2  8351  iooval2  10987  fzval2  11084  hashbc  11740  dfphi2  13201  phimullem  13206  mrcfval  13871  mrisval  13893  ipoval  14618  lspfval  16087  lsppropd  16132  rrgval  16385  aspval  16425  psrval  16467  mvrfval  16522  ltbval  16570  opsrval  16573  clsfval  17127  ordtrest  17304  ordtrest2lem  17305  ordtrest2  17306  xkoval  17657  xkopt  17725  qtopres  17768  kqval  17796  tsmsval2  18197  cncfval  18956  isphtpy  19044  cfilfval  19255  iscmet  19275  isumgra  21388  isuslgra  21410  isusgra  21411  orrvcval4  24757  orrvcoel  24758  orrvccel  24759  snmlfval  25052  funray  26109  fvray  26110  itg2addnclem2  26299  isptfin  26417  islocfin  26418  cntotbnd  26547  pellfundval  27055  dsmmbas2  27292  dsmmelbas  27294  frlmbas  27312  elmnc  27430  rgspnval  27462  pmtrfval  27482  psgnfval  27512  elovmpt3rab  28206  elovmpt2wrd  28311  elovmptnn0wrd  28312  wwlkn  28462  docaffvalN  32093  docafvalN  32094  lcfr  32557  hlhilocv  32932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2721
  Copyright terms: Public domain W3C validator