Theorem rabeq 3223

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 2793	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2793	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	rabeqf 3221	1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

Syntax hints:   → wi 4   = wceq 1523  {crab 2945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950

This theorem is referenced by:  rabeqdv  3225  difeq1  3754  ifeq1  4123  ifeq2  4124  elfvmptrab  6345  supp0  7345  suppvalfn  7347  suppsnop  7354  fnsuppres  7367  pmvalg  7910  supeq2  8395  oieq2  8459  scott0  8787  hsmex2  9293  iooval2  12246  fzval2  12367  hashbc  13275  elovmpt2wrd  13380  phimullem  15531  mrcfval  16315  ipoval  17201  psgnfval  17966  pmtrsn  17985  lspfval  19021  lsppropd  19066  rrgval  19335  aspval  19376  psrval  19410  mvrfval  19468  ltbval  19519  opsrval  19522  dsmmbas2  20129  dsmmelbas  20131  frlmbas  20147  m1detdiag  20451  clsfval  20877  ordtrest  21054  ordtrest2lem  21055  ordtrest2  21056  isptfin  21367  islocfin  21368  xkoval  21438  xkopt  21506  qtopres  21549  kqval  21577  tsmsval2  21980  cncfval  22738  isphtpy  22827  cfilfval  23108  iscmet  23128  ttgval  25800  uvtx0  26342  cusgredg  26376  cffldtocusgr  26399  vtxdg0e  26426  1hevtxdg1  26458  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  konigsbergiedgw  27226  ordtprsval  30092  ordtrestNEW  30095  ordtrest2NEWlem  30096  omsval  30483  orrvcval4  30654  orrvcoel  30655  orrvccel  30656  snmlfval  31438  funray  32372  fvray  32373  itg2addnclem2  33592  cntotbnd  33725  docaffvalN  36727  docafvalN  36728  lcfr  37191  hlhilocv  37566  pellfundval  37761  elmnc  38023  rgspnval  38055  rfovd  38612  fsovd  38619  fsovcnvlem  38624  ntrneibex  38688  k0004val0  38769  rabeqd  39590  dvnprodlem1  40479  dvnprodlem2  40480  dvnprodlem3  40481  dvnprod  40482  fvmptrab  41631  assintopmap  42167  rmsuppss  42476  mndpsuppss  42477  scmsuppss  42478  dmatALTval  42514  dmatALTbas  42515