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

Theorem raleq 3307
Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2137, ax-11 2154, and ax-12 2171. (Revised by Steven Nguyen, 30-Apr-2023.)
Assertion
Ref Expression
raleq (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleq
StepHypRef Expression
1 biidd 261 . 2 (𝐴 = 𝐵 → (𝜑𝜑))
21raleqbi1dv 3305 1 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  wral 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2729  df-ral 3063
This theorem is referenced by:  raleqi  3309  raleqdv  3311  sbralie  3330  r19.2zb  4451  inteq  4908  iineq1  4969  friOLD  5592  frsn  5717  fncnv  6571  isoeq4  7261  onminex  7729  tfisg  7782  tfinds  7788  f1oweALT  7897  frxp  8050  frxp2  8068  poseq  8082  frrlem1  8209  frrlem13  8221  wfrlem1OLD  8246  wfrlem15OLD  8261  tfrlem1  8314  tfrlem12  8327  omeulem1  8521  ixpeq1  8804  undifixp  8830  ac6sfi  9189  frfi  9190  iunfi  9242  indexfi  9262  supeq1  9339  supeq2  9342  brttrcl2  9608  ssttrcl  9609  ttrcltr  9610  bnd2  9787  acneq  9937  aceq3lem  10014  dfac5lem4  10020  dfac8  10029  dfac9  10030  kmlem1  10044  kmlem10  10053  kmlem13  10056  cfval  10141  axcc2lem  10330  axcc4dom  10335  axdc3lem3  10346  axdc3lem4  10347  ac4c  10370  ac5  10371  ac6sg  10382  zorn2lem7  10396  xrsupsslem  13180  xrinfmsslem  13181  xrsupss  13182  xrinfmss  13183  fsuppmapnn0fiubex  13851  rexanuz  15190  rexfiuz  15192  modfsummod  15639  gcdcllem3  16341  lcmfval  16457  lcmf0val  16458  lcmfunsnlem  16477  coprmprod  16497  coprmproddvds  16499  isprs  18146  drsdirfi  18154  isdrs2  18155  ispos  18163  pospropd  18176  lubeldm  18202  lubval  18205  glbeldm  18215  glbval  18218  istos  18267  isdlat  18371  mhmpropd  18568  isghm  18967  cntzval  19060  efgval  19458  iscmn  19530  dfrhm2  20101  lidldvgen  20678  ocvval  21024  isobs  21079  coe1fzgsumd  21625  evl1gsumd  21675  mat0dimcrng  21771  mdetunilem9  21921  ist0  22623  cmpcovf  22694  is1stc  22744  2ndc1stc  22754  isref  22812  txflf  23309  ustuqtop4  23548  iscfilu  23592  ispsmet  23609  ismet  23628  isxmet  23629  cncfval  24203  lebnumlem3  24278  fmcfil  24588  iscfil3  24589  caucfil  24599  iscmet3  24609  cfilres  24612  minveclem3  24745  ovolfiniun  24817  finiunmbl  24860  volfiniun  24863  dvcn  25237  ulmval  25691  sltval2  26956  sltres  26962  nolesgn2o  26971  nogesgn1o  26973  nodense  26992  nosupbnd2lem1  27015  noinfbnd2lem1  27030  brsslt  27077  madebday  27178  axtgcont1  27239  nb3grpr  28159  dfconngr1  28961  isconngr  28962  1conngr  28967  frgr0v  29035  isplig  29247  isgrpo  29268  isablo  29317  ocval  30051  acunirnmpt  31404  isomnd  31735  isorng  31920  prmidl  32034  ismbfm  32662  bnj865  33347  bnj1154  33423  bnj1296  33445  bnj1463  33479  derangval  33573  setinds  34169  dfon2lem3  34176  dfon2lem7  34180  negsprop  34328  dfrecs2  34473  dfrdg4  34474  isfne  34749  finixpnum  36001  mblfinlem1  36053  mbfresfi  36062  indexdom  36131  heibor1lem  36206  isexid2  36252  ismndo2  36271  rngomndo  36332  pridl  36434  smprngopr  36449  ispridlc  36467  setindtrs  41258  dford3lem2  41260  dfac11  41298  rp-intrabeq  41464  rp-unirabeq  41465  rp-brsslt  41606  mnuop123d  42453  fnchoice  43145  axccdom  43348  axccd  43355  stoweidlem31  44173  stoweidlem57  44199  fourierdlem80  44328  fourierdlem103  44351  fourierdlem104  44352  isvonmbl  44780  paireqne  45604  requad2  45716  mgmhmpropd  45980  rnghmval  46090  zrrnghm  46116  isthinc  46942  0thincg  46971  bnd2d  47027
  Copyright terms: Public domain W3C validator