MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabeq Structured version   Visualization version   GIF version

Theorem rabeq 3483
Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2141, ax-11 2157, ax-12 2173. (Revised by Gino Giotto, 20-Aug-2023.)
Assertion
Ref Expression
rabeq (𝐴 = 𝐵 → {𝑥𝐴𝜑} = {𝑥𝐵𝜑})
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabeq
StepHypRef Expression
1 eleq2 2901 . . 3 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21anbi1d 631 . 2 (𝐴 = 𝐵 → ((𝑥𝐴𝜑) ↔ (𝑥𝐵𝜑)))
32rabbidva2 3476 1 (𝐴 = 𝐵 → {𝑥𝐴𝜑} = {𝑥𝐵𝜑})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  wcel 2110  {crab 3142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147
This theorem is referenced by:  rabeqdv  3484  difeq1  4091  ineq1  4180  ifeq1  4470  ifeq2  4471  elfvmptrab  6795  supp0  7834  supeq2  8911  oieq2  8976  scott0  9314  mrcfval  16878  ipoval  17763  psgnfval  18627  lsppropd  19789  psrval  20141  ltbval  20251  opsrval  20254  dsmmelbas  20882  m1detdiag  21205  isptfin  22123  islocfin  22124  kqval  22333  incistruhgr  26863  uvtx0  27175  vtxdg0e  27255  1hevtxdg1  27287  hashecclwwlkn1  27855  umgrhashecclwwlk  27856  ordtrestNEW  31164  ordtrest2NEWlem  31165  omsval  31551  orrvcval4  31722  orrvcoel  31723  orrvccel  31724  funray  33601  fvray  33602  itg2addnclem2  34943  cntotbnd  35073  lcfr  38720  hlhilocv  39092  pellfundval  39475  elmnc  39734  rgspnval  39766  rfovd  40345  fsovd  40352  fsovcnvlem  40357  ntrneibex  40421  dvnprodlem1  42229  dvnprodlem2  42230  dvnprodlem3  42231  dvnprod  42232  fvmptrab  43490  rmsuppss  44417  mndpsuppss  44418  scmsuppss  44419  dmatALTbas  44455
  Copyright terms: Public domain W3C validator