Theorem rabeq 3485

Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2145, ax-11 2161, ax-12 2177. (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 2903	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	rabbidva2 3478	1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  {crab 3144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-rab 3149

This theorem is referenced by:  rabeqdv  3486  difeq1  4094  ineq1  4183  ifeq1  4473  ifeq2  4474  elfvmptrab  6798  supp0  7837  supeq2  8914  oieq2  8979  scott0  9317  mrcfval  16881  ipoval  17766  psgnfval  18630  lsppropd  19792  psrval  20144  ltbval  20254  opsrval  20257  dsmmelbas  20885  m1detdiag  21208  isptfin  22126  islocfin  22127  kqval  22336  incistruhgr  26866  uvtx0  27178  vtxdg0e  27258  1hevtxdg1  27290  hashecclwwlkn1  27858  umgrhashecclwwlk  27859  ordtrestNEW  31166  ordtrest2NEWlem  31167  omsval  31553  orrvcval4  31724  orrvcoel  31725  orrvccel  31726  funray  33603  fvray  33604  itg2addnclem2  34946  cntotbnd  35076  lcfr  38723  hlhilocv  39095  pellfundval  39484  elmnc  39743  rgspnval  39775  rfovd  40354  fsovd  40361  fsovcnvlem  40366  ntrneibex  40430  dvnprodlem1  42238  dvnprodlem2  42239  dvnprodlem3  42240  dvnprod  42241  fvmptrab  43498  rmsuppss  44425  mndpsuppss  44426  scmsuppss  44427  dmatALTbas  44463