Theorem rabeq 3418

Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2137, ax-11 2154, ax-12 2171. (Revised by Gino Giotto, 20-Aug-2023.)

Assertion

Ref	Expression
rabeq	⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabeq

Step	Hyp	Ref	Expression
1		eleq2 2827	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 630	. 2 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	rabbidva2 3411	1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  {crab 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073

This theorem is referenced by:  rabeqdv  3419  difeq1  4050  ineq1  4139  ifeq1  4463  ifeq2  4464  elfvmptrab  6903  supp0  7982  supeq2  9207  oieq2  9272  scott0  9644  mrcfval  17317  ipoval  18248  psgnfval  19108  dsmmelbas  20946  psrval  21118  ltbval  21244  opsrval  21247  m1detdiag  21746  isptfin  22667  islocfin  22668  kqval  22877  incistruhgr  27449  uvtx0  27761  vtxdg0e  27841  1hevtxdg1  27873  hashecclwwlkn1  28441  umgrhashecclwwlk  28442  ordtrestNEW  31871  ordtrest2NEWlem  31872  omsval  32260  orrvcval4  32431  orrvcoel  32432  orrvccel  32433  funray  34442  fvray  34443  itg2addnclem2  35829  cntotbnd  35954  lcfr  39599  hlhilocv  39975  pellfundval  40702  elmnc  40961  rgspnval  40993  rfovd  41609  fsovd  41616  fsovcnvlem  41621  ntrneibex  41683  dvnprodlem1  43487  dvnprodlem2  43488  dvnprodlem3  43489  dvnprod  43490  fvmptrab  44784  rmsuppss  45706  mndpsuppss  45707  scmsuppss  45708  dmatALTbas  45742