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

Theorem rabeq 2858
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 2494 . 2  |-  F/_ x A
2 nfcv 2494 . 2  |-  F/_ x B
31, 2rabeqf 2857 1  |-  ( A  =  B  ->  { x  e.  A  |  ph }  =  { x  e.  B  |  ph } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642   {crab 2623
This theorem is referenced by:  rabeqbidv  2859  rabeqbidva  2860  difeq1  3363  ifeq1  3645  ifeq2  3646  pmvalg  6868  supeq2  7288  oieq2  7315  cantnffval  7451  scott0  7643  hsmex2  8146  iooval2  10778  fzval2  10874  hashbc  11481  dfphi2  12933  phimullem  12938  mrcfval  13603  mrisval  13625  ipoval  14350  lspfval  15823  lsppropd  15868  rrgval  16121  aspval  16161  psrval  16203  mvrfval  16258  ltbval  16306  opsrval  16309  clsfval  16862  ordtrest  17032  ordtrest2lem  17033  ordtrest2  17034  xkoval  17382  xkopt  17449  qtopres  17489  kqval  17517  tsmsval2  17908  cncfval  18489  isphtpy  18577  cfilfval  18788  iscmet  18808  orrvcval4  23971  orrvcoel  23972  orrvccel  23973  isumgra  24271  snmlfval  24317  funray  25322  fvray  25323  itg2addnclem2  25493  isptfin  25619  islocfin  25620  cntotbnd  25843  pellfundval  26288  dsmmbas2  26526  dsmmelbas  26528  frlmbas  26546  elmnc  26664  rgspnval  26696  pmtrfval  26716  psgnfval  26746  rabrsn  27410  isuslgra  27519  isusgra  27520  docaffvalN  31363  docafvalN  31364  lcfr  31827  hlhilocv  32202
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rab 2628
  Copyright terms: Public domain W3C validator