Theorem rabeq 3438

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  {crab 3424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425

This theorem is referenced by:  rabeqdv  3439  difeq1  4107  ineq1  4197  ifeq1  4524  ifeq2  4525  elfvmptrab  7016  supp0  8145  supeq2  9439  oieq2  9504  scott0  9877  mrcfval  17551  ipoval  18485  psgnfval  19410  dsmmelbas  21602  psrval  21777  ltbval  21908  opsrval  21911  m1detdiag  22421  isptfin  23342  islocfin  23343  kqval  23552  incistruhgr  28808  uvtx0  29120  vtxdg0e  29200  1hevtxdg1  29232  hashecclwwlkn1  29799  umgrhashecclwwlk  29800  ordtrestNEW  33390  ordtrest2NEWlem  33391  omsval  33781  orrvcval4  33952  orrvcoel  33953  orrvccel  33954  funray  35607  fvray  35608  itg2addnclem2  37030  cntotbnd  37154  lcfr  40946  hlhilocv  41322  pellfundval  42107  elmnc  42367  rgspnval  42399  rfovd  43241  fsovd  43248  fsovcnvlem  43253  ntrneibex  43313  dvnprodlem1  45147  dvnprodlem2  45148  dvnprodlem3  45149  dvnprod  45150  fvmptrab  46485  rmsuppss  47235  mndpsuppss  47236  scmsuppss  47237  dmatALTbas  47270