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

Theorem rabeq 3340
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 2906 . 2 𝑥𝐴
2 nfcv 2906 . 2 𝑥𝐵
31, 2rabeqf 3338 1 (𝐴 = 𝐵 → {𝑥𝐴𝜑} = {𝑥𝐵𝜑})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  {crab 3058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-rab 3063
This theorem is referenced by:  rabeqdv  3342  difeq1  3882  ifeq1  4246  ifeq2  4247  elfvmptrab  6494  supp0  7501  suppvalfn  7503  suppsnop  7510  fnsuppres  7524  pmvalg  8070  supeq2  8560  oieq2  8624  scott0  8963  hsmex2  9507  iooval2  12409  fzval2  12535  hashbc  13437  elovmpt2wrd  13528  phimullem  15764  mrcfval  16535  ipoval  17421  psgnfval  18185  pmtrsn  18204  lspfval  19244  lsppropd  19289  rrgval  19560  aspval  19601  psrval  19635  mvrfval  19693  ltbval  19744  opsrval  19747  dsmmbas2  20356  dsmmelbas  20358  frlmbas  20374  m1detdiag  20679  clsfval  21108  ordtrest  21285  ordtrest2lem  21286  ordtrest2  21287  isptfin  21598  islocfin  21599  xkoval  21669  xkopt  21737  qtopres  21780  kqval  21808  tsmsval2  22211  cncfval  22969  isphtpy  23058  cfilfval  23340  iscmet  23360  ttgval  26045  uvtx0  26576  cusgredg  26610  cffldtocusgr  26633  vtxdg0e  26660  1hevtxdg1  26692  hashecclwwlkn1  27290  umgrhashecclwwlk  27291  konigsbergiedgw  27483  ordtprsval  30345  ordtrestNEW  30348  ordtrest2NEWlem  30349  omsval  30736  orrvcval4  30908  orrvcoel  30909  orrvccel  30910  snmlfval  31691  funray  32622  fvray  32623  itg2addnclem2  33817  cntotbnd  33949  docaffvalN  37009  docafvalN  37010  lcfr  37473  hlhilocv  37845  pellfundval  38054  elmnc  38315  rgspnval  38347  rfovd  38901  fsovd  38908  fsovcnvlem  38913  ntrneibex  38977  k0004val0  39058  rabeqd  39859  dvnprodlem1  40731  dvnprodlem2  40732  dvnprodlem3  40733  dvnprod  40734  fvmptrab  41973  assintopmap  42443  rmsuppss  42752  mndpsuppss  42753  scmsuppss  42754  dmatALTval  42790  dmatALTbas  42791
  Copyright terms: Public domain W3C validator