Theorem rabeq 3405

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  {crab 3391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392

This theorem is referenced by:  rabeqdv  3406  difeq1  4050  ineq1  4142  ifeq1  4458  ifeq2  4459  elfvmptrab  6965  supp0  8105  supeq2  9351  oieq2  9418  scott0  9801  mrcfval  17565  ipoval  18487  chneq2  18570  mndpsuppss  18724  psgnfval  19466  rgspnval  20584  dsmmelbas  21714  psrval  21890  ltbval  22019  opsrval  22022  m1detdiag  22580  isptfin  23499  islocfin  23500  kqval  23709  incistruhgr  29166  uvtx0  29481  vtxdg0e  29561  1hevtxdg1  29593  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  ordtrestNEW  34105  ordtrest2NEWlem  34106  omsval  34477  orrvcval4  34649  orrvcoel  34650  orrvccel  34651  funray  36368  fvray  36369  itg2addnclem2  38039  cntotbnd  38163  lcfr  42077  hlhilocv  42449  pellfundval  43325  elmnc  43581  rfovd  44445  fsovd  44452  fsovcnvlem  44457  ntrneibex  44517  dvnprodlem2  46390  dvnprodlem3  46391  dvnprod  46392  fvmptrab  47755  rmsuppss  48861  scmsuppss  48862  dmatALTbas  48892