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

Theorem rabeq 2782
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 2419 . 2  |-  F/_ x A
2 nfcv 2419 . 2  |-  F/_ x B
31, 2rabeqf 2781 1  |-  ( A  =  B  ->  { x  e.  A  |  ph }  =  { x  e.  B  |  ph } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   {crab 2547
This theorem is referenced by:  rabeqbidv  2783  rabeqbidva  2784  difeq1  3287  ifeq1  3569  ifeq2  3570  pmvalg  6783  supeq2  7201  oieq2  7228  cantnffval  7364  scott0  7556  hsmex2  8059  iooval2  10689  fzval2  10785  hashbc  11391  dfphi2  12842  phimullem  12847  mrcfval  13510  mrisval  13532  ipoval  14257  lspfval  15730  lsppropd  15775  rrgval  16028  aspval  16068  psrval  16110  mvrfval  16165  ltbval  16213  opsrval  16216  clsfval  16762  ordtrest  16932  ordtrest2lem  16933  ordtrest2  16934  xkoval  17282  xkopt  17349  qtopres  17389  kqval  17417  tsmsval2  17812  cncfval  18392  isphtpy  18479  cfilfval  18690  iscmet  18710  orrvcval4  23665  orrvcoel  23666  orrvccel  23667  isumgra  23867  snmlfval  23913  funray  24763  fvray  24764  ubos  25256  ubos2  25257  isnword  25986  isptfin  26295  islocfin  26296  cntotbnd  26520  pellfundval  26965  dsmmbas2  27203  dsmmelbas  27205  frlmbas  27223  elmnc  27341  rgspnval  27373  pmtrfval  27393  psgnfval  27423  isuslgra  28102  isusgra  28103  docaffvalN  31311  docafvalN  31312  lcfr  31775  hlhilocv  32150
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552
  Copyright terms: Public domain W3C validator