Theorem rabeq 3458

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  {crab 3443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444

This theorem is referenced by:  rabeqdv  3459  difeq1  4142  ineq1  4234  ifeq1  4552  ifeq2  4553  elfvmptrab  7058  supp0  8206  supeq2  9517  oieq2  9582  scott0  9955  mrcfval  17666  ipoval  18600  psgnfval  19542  dsmmelbas  21782  psrval  21958  ltbval  22084  opsrval  22087  m1detdiag  22624  isptfin  23545  islocfin  23546  kqval  23755  incistruhgr  29114  uvtx0  29429  vtxdg0e  29510  1hevtxdg1  29542  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  ordtrestNEW  33867  ordtrest2NEWlem  33868  omsval  34258  orrvcval4  34429  orrvcoel  34430  orrvccel  34431  funray  36104  fvray  36105  itg2addnclem2  37632  cntotbnd  37756  lcfr  41542  hlhilocv  41918  pellfundval  42836  elmnc  43093  rgspnval  43125  rfovd  43963  fsovd  43970  fsovcnvlem  43975  ntrneibex  44035  dvnprodlem1  45867  dvnprodlem2  45868  dvnprodlem3  45869  dvnprod  45870  fvmptrab  47207  rmsuppss  48095  mndpsuppss  48096  scmsuppss  48097  dmatALTbas  48130