Theorem rabeq 3418

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

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132  {crab 3404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405

This theorem is referenced by:  rabeqdv  3419  difeq1  4064  ineq1  4156  ifeq1  4474  ifeq2  4475  elfvmptrab  6990  supp0  8129  supeq2  9380  oieq2  9447  scott0  9830  mrcfval  17612  ipoval  18534  chneq2  18617  mndpsuppss  18771  psgnfval  19512  rgspnval  20630  dsmmelbas  21760  psrval  21936  ltbval  22065  opsrval  22068  m1detdiag  22626  isptfin  23545  islocfin  23546  kqval  23755  incistruhgr  29215  uvtx0  29530  vtxdg0e  29610  1hevtxdg1  29642  hashecclwwlkn1  30214  umgrhashecclwwlk  30215  ordtrestNEW  34162  ordtrest2NEWlem  34163  omsval  34534  orrvcval4  34706  orrvcoel  34707  orrvccel  34708  funray  36428  fvray  36429  itg2addnclem2  38109  cntotbnd  38233  lcfr  42147  hlhilocv  42519  pellfundval  43395  elmnc  43651  rfovd  44515  fsovd  44522  fsovcnvlem  44527  ntrneibex  44587  dvnprodlem2  46459  dvnprodlem3  46460  dvnprod  46461  fvmptrab  47824  rmsuppss  48930  scmsuppss  48931  dmatALTbas  48961