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

Theorem rabeq 3342
Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.)
Assertion
Ref Expression
rabeq (𝐴 = 𝐵 → {𝑥𝐴𝜑} = {𝑥𝐵𝜑})
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabeq
StepHypRef Expression
1 nfcv 2913 . 2 𝑥𝐴
2 nfcv 2913 . 2 𝑥𝐵
31, 2rabeqf 3340 1 (𝐴 = 𝐵 → {𝑥𝐴𝜑} = {𝑥𝐵𝜑})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  {crab 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070
This theorem is referenced by:  rabeqdv  3344  difeq1  3872  ifeq1  4229  ifeq2  4230  elfvmptrab  6446  supp0  7449  suppvalfn  7451  suppsnop  7458  fnsuppres  7472  pmvalg  8018  supeq2  8508  oieq2  8572  scott0  8911  hsmex2  9455  iooval2  12406  fzval2  12529  hashbc  13432  elovmpt2wrd  13537  phimullem  15684  mrcfval  16469  ipoval  17355  psgnfval  18120  pmtrsn  18139  lspfval  19179  lsppropd  19224  rrgval  19495  aspval  19536  psrval  19570  mvrfval  19628  ltbval  19679  opsrval  19682  dsmmbas2  20291  dsmmelbas  20293  frlmbas  20309  m1detdiag  20614  clsfval  21043  ordtrest  21220  ordtrest2lem  21221  ordtrest2  21222  isptfin  21533  islocfin  21534  xkoval  21604  xkopt  21672  qtopres  21715  kqval  21743  tsmsval2  22146  cncfval  22904  isphtpy  22993  cfilfval  23274  iscmet  23294  ttgval  25969  uvtx0  26514  cusgredg  26548  cffldtocusgr  26571  vtxdg0e  26598  1hevtxdg1  26630  hashecclwwlkn1  27228  umgrhashecclwwlk  27229  konigsbergiedgw  27421  ordtprsval  30297  ordtrestNEW  30300  ordtrest2NEWlem  30301  omsval  30688  orrvcval4  30859  orrvcoel  30860  orrvccel  30861  snmlfval  31643  funray  32577  fvray  32578  itg2addnclem2  33787  cntotbnd  33920  docaffvalN  36924  docafvalN  36925  lcfr  37388  hlhilocv  37760  pellfundval  37963  elmnc  38225  rgspnval  38257  rfovd  38814  fsovd  38821  fsovcnvlem  38826  ntrneibex  38890  k0004val0  38971  rabeqd  39790  dvnprodlem1  40672  dvnprodlem2  40673  dvnprodlem3  40674  dvnprod  40675  fvmptrab  41827  assintopmap  42363  rmsuppss  42672  mndpsuppss  42673  scmsuppss  42674  dmatALTval  42710  dmatALTbas  42711
  Copyright terms: Public domain W3C validator