Theorem rabeq 3428

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  {crab 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415

This theorem is referenced by:  rabeqdv  3429  difeq1  4073  ineq1  4165  ifeq1  4484  ifeq2  4485  elfvmptrab  7005  supp0  8145  supeq2  9394  oieq2  9461  scott0  9844  mrcfval  17640  ipoval  18562  chneq2  18645  mndpsuppss  18799  psgnfval  19540  rgspnval  20662  dsmmelbas  21791  psrval  21967  ltbval  22096  opsrval  22099  m1detdiag  22657  isptfin  23576  islocfin  23577  kqval  23786  incistruhgr  29280  uvtx0  29595  vtxdg0e  29675  1hevtxdg1  29707  hashecclwwlkn1  30279  umgrhashecclwwlk  30280  ordtrestNEW  34218  ordtrest2NEWlem  34219  omsval  34590  orrvcval4  34762  orrvcoel  34763  orrvccel  34764  funray  36490  fvray  36491  itg2addnclem2  38171  cntotbnd  38295  lcfr  42209  hlhilocv  42581  pellfundval  43457  elmnc  43713  rfovd  44577  fsovd  44584  fsovcnvlem  44589  ntrneibex  44649  dvnprodlem2  46521  dvnprodlem3  46522  dvnprod  46523  fvmptrab  47886  rmsuppss  48992  scmsuppss  48993  dmatALTbas  49023