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

Theorem rabeq 3182
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 2761 . 2 𝑥𝐴
2 nfcv 2761 . 2 𝑥𝐵
31, 2rabeqf 3181 1 (𝐴 = 𝐵 → {𝑥𝐴𝜑} = {𝑥𝐵𝜑})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  {crab 2911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916
This theorem is referenced by:  rabeqdv  3183  difeq1  3704  ifeq1  4067  ifeq2  4068  elfvmptrab  6267  supp0  7252  suppvalfn  7254  suppsnop  7261  fnsuppres  7274  pmvalg  7820  supeq2  8305  oieq2  8369  scott0  8700  hsmex2  9206  iooval2  12157  fzval2  12278  hashbc  13182  elovmpt2wrd  13293  phimullem  15415  mrcfval  16196  ipoval  17082  psgnfval  17848  pmtrsn  17867  lspfval  18901  lsppropd  18946  rrgval  19215  aspval  19256  psrval  19290  mvrfval  19348  ltbval  19399  opsrval  19402  dsmmbas2  20009  dsmmelbas  20011  frlmbas  20027  m1detdiag  20331  clsfval  20748  ordtrest  20925  ordtrest2lem  20926  ordtrest2  20927  isptfin  21238  islocfin  21239  xkoval  21309  xkopt  21377  qtopres  21420  kqval  21448  tsmsval2  21852  cncfval  22610  isphtpy  22699  cfilfval  22981  iscmet  23001  ttgval  25668  uvtxa0  26194  cusgredg  26220  cffldtocusgr  26243  vtxdg0e  26269  1hevtxdg1  26301  hashecclwwlksn1  26833  umgrhashecclwwlk  26834  konigsbergiedgw  26987  konigsbergiedgwOLD  26988  ordtprsval  29764  ordtrestNEW  29767  ordtrest2NEWlem  29768  omsval  30154  orrvcval4  30325  orrvcoel  30326  orrvccel  30327  snmlfval  31047  funray  31916  fvray  31917  itg2addnclem2  33121  cntotbnd  33254  docaffvalN  35917  docafvalN  35918  lcfr  36381  hlhilocv  36756  pellfundval  36951  elmnc  37214  rgspnval  37246  rfovd  37804  fsovd  37811  fsovcnvlem  37816  ntrneibex  37880  k0004val0  37961  rabeqd  38786  dvnprodlem1  39489  dvnprodlem2  39490  dvnprodlem3  39491  dvnprod  39492  assintopmap  41151  rmsuppss  41460  mndpsuppss  41461  scmsuppss  41462  dmatALTval  41498  dmatALTbas  41499
  Copyright terms: Public domain W3C validator