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

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

Proof of Theorem rabeq
StepHypRef Expression
1 eleq2 2830 . . 3 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21anbi1d 631 . 2 (𝐴 = 𝐵 → ((𝑥𝐴𝜑) ↔ (𝑥𝐵𝜑)))
32rabbidva2 3438 1 (𝐴 = 𝐵 → {𝑥𝐴𝜑} = {𝑥𝐵𝜑})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2108  {crab 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437
This theorem is referenced by:  rabeqdv  3452  difeq1  4119  ineq1  4213  ifeq1  4529  ifeq2  4530  elfvmptrab  7045  supp0  8190  supeq2  9488  oieq2  9553  scott0  9926  mrcfval  17651  ipoval  18575  mndpsuppss  18778  psgnfval  19518  rgspnval  20612  dsmmelbas  21759  psrval  21935  ltbval  22061  opsrval  22064  m1detdiag  22603  isptfin  23524  islocfin  23525  kqval  23734  incistruhgr  29096  uvtx0  29411  vtxdg0e  29492  1hevtxdg1  29524  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  ordtrestNEW  33920  ordtrest2NEWlem  33921  omsval  34295  orrvcval4  34467  orrvcoel  34468  orrvccel  34469  funray  36141  fvray  36142  itg2addnclem2  37679  cntotbnd  37803  lcfr  41587  hlhilocv  41963  pellfundval  42891  elmnc  43148  rfovd  44014  fsovd  44021  fsovcnvlem  44026  ntrneibex  44086  dvnprodlem2  45962  dvnprodlem3  45963  dvnprod  45964  fvmptrab  47304  rmsuppss  48286  scmsuppss  48287  dmatALTbas  48318
  Copyright terms: Public domain W3C validator