Theorem rabeq 3437

Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2182, ax-11 2198, ax-12 2219. (Revised by GG, 20-Aug-2023.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabeq

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424

This theorem is referenced by:  rabeqdv  3438  difeq1  4082  ineq1  4174  ifeq1  4496  ifeq2  4497  elfvmptrab  7020  supp0  8161  supeq2  9408  oieq2  9475  scott0  9860  mrcfval  17664  ipoval  18586  chneq2  18669  mndpsuppss  18823  psgnfval  19570  rgspnval  20697  dsmmelbas  21858  psrval  22034  ltbval  22163  opsrval  22166  m1detdiag  22723  isptfin  23642  islocfin  23643  kqval  23852  incistruhgr  29370  uvtx0  29685  vtxdg0e  29765  1hevtxdg1  29797  hashecclwwlkn1  30369  umgrhashecclwwlk  30370  ordtrestNEW  34256  ordtrest2NEWlem  34257  omsval  34628  orrvcval4  34800  orrvcoel  34801  orrvccel  34802  funray  36531  fvray  36532  itg2addnclem2  38211  cntotbnd  38335  lcfr  42249  hlhilocv  42621  pellfundval  43499  elmnc  43755  rfovd  44619  fsovd  44626  fsovcnvlem  44631  ntrneibex  44691  dvnprodlem2  46553  dvnprodlem3  46554  dvnprod  46555  fvmptrab  47918  rmsuppss  49035  scmsuppss  49036  dmatALTbas  49066