Theorem rabeq 3166

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

Step	Hyp	Ref	Expression
1		nfcv 2751	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2751	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	rabeqf 3165	1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

Syntax hints:   → wi 4   = wceq 1475  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905

This theorem is referenced by:  rabeqdv  3167  difeq1  3683  ifeq1  4040  ifeq2  4041  elfvmptrab  6214  supp0  7187  suppvalfn  7189  suppsnop  7196  fnsuppres  7209  pmvalg  7755  supeq2  8237  oieq2  8301  scott0  8632  hsmex2  9138  iooval2  12079  fzval2  12200  hashbc  13094  elovmpt2wrd  13202  phimullem  15322  mrcfval  16091  ipoval  16977  psgnfval  17743  pmtrsn  17762  lspfval  18794  lsppropd  18839  rrgval  19108  aspval  19149  psrval  19183  mvrfval  19241  ltbval  19292  opsrval  19295  dsmmbas2  19900  dsmmelbas  19902  frlmbas  19918  m1detdiag  20222  clsfval  20639  ordtrest  20816  ordtrest2lem  20817  ordtrest2  20818  isptfin  21129  islocfin  21130  xkoval  21200  xkopt  21268  qtopres  21311  kqval  21339  tsmsval2  21743  cncfval  22499  isphtpy  22588  cfilfval  22870  iscmet  22890  ttgval  25555  isumgra  25844  isuslgra  25872  isusgra  25873  edgss  25881  wwlkn  26210  clwwlkn  26295  hashecclwwlkn1  26361  usghashecclwwlk  26362  rusgrasn  26472  numclwwlkovf2  26611  numclwwlkqhash  26627  ordtprsval  29292  ordtrestNEW  29295  ordtrest2NEWlem  29296  omsval  29682  orrvcval4  29853  orrvcoel  29854  orrvccel  29855  snmlfval  30566  funray  31417  fvray  31418  itg2addnclem2  32632  cntotbnd  32765  docaffvalN  35428  docafvalN  35429  lcfr  35892  hlhilocv  36267  pellfundval  36462  elmnc  36725  rgspnval  36757  rfovd  37315  fsovd  37322  fsovcnvlem  37327  ntrneibex  37391  k0004val0  37472  rabeqd  38304  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  dvnprod  38839  uvtxa0  40620  cusgredg  40646  vtxdg0e  40689  1hevtxdg1  40721  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  konigsbergiedgw  41416  konigsbergiedgwOLD  41417  assintopmap  41632  rmsuppss  41945  mndpsuppss  41946  scmsuppss  41947  dmatALTval  41983  dmatALTbas  41984