Theorem rabeq 3413

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {crab 3399

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400

This theorem is referenced by:  rabeqdv  3414  difeq1  4071  ineq1  4165  ifeq1  4483  ifeq2  4484  elfvmptrab  6970  supp0  8107  supeq2  9351  oieq2  9418  scott0  9798  mrcfval  17531  ipoval  18453  chneq2  18536  mndpsuppss  18690  psgnfval  19429  rgspnval  20545  dsmmelbas  21694  psrval  21871  ltbval  21998  opsrval  22001  m1detdiag  22541  isptfin  23460  islocfin  23461  kqval  23670  incistruhgr  29152  uvtx0  29467  vtxdg0e  29548  1hevtxdg1  29580  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  ordtrestNEW  34078  ordtrest2NEWlem  34079  omsval  34450  orrvcval4  34622  orrvcoel  34623  orrvccel  34624  funray  36334  fvray  36335  itg2addnclem2  37873  cntotbnd  37997  lcfr  41855  hlhilocv  42227  pellfundval  43132  elmnc  43388  rfovd  44252  fsovd  44259  fsovcnvlem  44264  ntrneibex  44324  dvnprodlem2  46201  dvnprodlem3  46202  dvnprod  46203  fvmptrab  47548  rmsuppss  48626  scmsuppss  48627  dmatALTbas  48657