Theorem rabeq 3447

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  {crab 3433

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434

This theorem is referenced by:  rabeqdv  3448  difeq1  4116  ineq1  4206  ifeq1  4533  ifeq2  4534  elfvmptrab  7027  supp0  8151  supeq2  9443  oieq2  9508  scott0  9881  mrcfval  17552  ipoval  18483  psgnfval  19368  dsmmelbas  21294  psrval  21468  ltbval  21598  opsrval  21601  m1detdiag  22099  isptfin  23020  islocfin  23021  kqval  23230  incistruhgr  28339  uvtx0  28651  vtxdg0e  28731  1hevtxdg1  28763  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  ordtrestNEW  32901  ordtrest2NEWlem  32902  omsval  33292  orrvcval4  33463  orrvcoel  33464  orrvccel  33465  funray  35112  fvray  35113  itg2addnclem2  36540  cntotbnd  36664  lcfr  40456  hlhilocv  40832  pellfundval  41618  elmnc  41878  rgspnval  41910  rfovd  42752  fsovd  42759  fsovcnvlem  42764  ntrneibex  42824  dvnprodlem1  44662  dvnprodlem2  44663  dvnprodlem3  44664  dvnprod  44665  fvmptrab  46000  rmsuppss  47046  mndpsuppss  47047  scmsuppss  47048  dmatALTbas  47082