Theorem rabeq 3192

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

Syntax hints:   → wi 4   = wceq 1483  {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921

This theorem is referenced by:  rabeqdv  3194  difeq1  3721  ifeq1  4090  ifeq2  4091  elfvmptrab  6306  supp0  7300  suppvalfn  7302  suppsnop  7309  fnsuppres  7322  pmvalg  7868  supeq2  8354  oieq2  8418  scott0  8749  hsmex2  9255  iooval2  12208  fzval2  12329  hashbc  13237  elovmpt2wrd  13347  phimullem  15484  mrcfval  16268  ipoval  17154  psgnfval  17920  pmtrsn  17939  lspfval  18973  lsppropd  19018  rrgval  19287  aspval  19328  psrval  19362  mvrfval  19420  ltbval  19471  opsrval  19474  dsmmbas2  20081  dsmmelbas  20083  frlmbas  20099  m1detdiag  20403  clsfval  20829  ordtrest  21006  ordtrest2lem  21007  ordtrest2  21008  isptfin  21319  islocfin  21320  xkoval  21390  xkopt  21458  qtopres  21501  kqval  21529  tsmsval2  21933  cncfval  22691  isphtpy  22780  cfilfval  23062  iscmet  23082  ttgval  25755  uvtxa0  26294  cusgredg  26320  cffldtocusgr  26343  vtxdg0e  26370  1hevtxdg1  26402  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  konigsbergiedgw  27108  konigsbergiedgwOLD  27109  ordtprsval  29964  ordtrestNEW  29967  ordtrest2NEWlem  29968  omsval  30355  orrvcval4  30526  orrvcoel  30527  orrvccel  30528  snmlfval  31312  funray  32247  fvray  32248  itg2addnclem2  33462  cntotbnd  33595  docaffvalN  36410  docafvalN  36411  lcfr  36874  hlhilocv  37249  pellfundval  37444  elmnc  37706  rgspnval  37738  rfovd  38295  fsovd  38302  fsovcnvlem  38307  ntrneibex  38371  k0004val0  38452  rabeqd  39276  dvnprodlem1  40161  dvnprodlem2  40162  dvnprodlem3  40163  dvnprod  40164  assintopmap  41842  rmsuppss  42151  mndpsuppss  42152  scmsuppss  42153  dmatALTval  42189  dmatALTbas  42190