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

Theorem rabeq 2918
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 2548 . 2  |-  F/_ x A
2 nfcv 2548 . 2  |-  F/_ x B
31, 2rabeqf 2917 1  |-  ( A  =  B  ->  { x  e.  A  |  ph }  =  { x  e.  B  |  ph } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   {crab 2678
This theorem is referenced by:  rabeqbidv  2919  rabeqbidva  2920  difeq1  3426  ifeq1  3711  ifeq2  3712  rabrsn  3842  pmvalg  6996  supeq2  7419  oieq2  7446  cantnffval  7582  scott0  7774  hsmex2  8277  iooval2  10913  fzval2  11010  hashbc  11665  dfphi2  13126  phimullem  13131  mrcfval  13796  mrisval  13818  ipoval  14543  lspfval  16012  lsppropd  16057  rrgval  16310  aspval  16350  psrval  16392  mvrfval  16447  ltbval  16495  opsrval  16498  clsfval  17052  ordtrest  17228  ordtrest2lem  17229  ordtrest2  17230  xkoval  17580  xkopt  17648  qtopres  17691  kqval  17719  tsmsval2  18120  cncfval  18879  isphtpy  18967  cfilfval  19178  iscmet  19198  isumgra  21311  isuslgra  21333  isusgra  21334  orrvcval4  24683  orrvcoel  24684  orrvccel  24685  snmlfval  24978  funray  25986  fvray  25987  itg2addnclem2  26164  isptfin  26273  islocfin  26274  cntotbnd  26403  pellfundval  26841  dsmmbas2  27079  dsmmelbas  27081  frlmbas  27099  elmnc  27217  rgspnval  27249  pmtrfval  27269  psgnfval  27299  docaffvalN  31616  docafvalN  31617  lcfr  32080  hlhilocv  32455
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rab 2683
  Copyright terms: Public domain W3C validator