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

Theorem raleq 3403
Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2136, ax-11 2151, and ax-12 2167. (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 263 . 2 (𝐴 = 𝐵 → (𝜑𝜑))
21raleqbi1dv 3401 1 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  df-ral 3140
This theorem is referenced by:  raleqi  3411  raleqdv  3413  raleqbi1dvOLD  3415  sbralie  3469  r19.2zb  4437  inteq  4870  iineq1  4927  fri  5510  frsn  5632  fncnv  6420  isoeq4  7062  onminex  7511  tfinds  7563  f1oweALT  7662  frxp  7809  wfrlem1  7943  wfrlem15  7958  tfrlem1  8001  tfrlem12  8014  omeulem1  8197  ixpeq1  8460  undifixp  8486  ac6sfi  8750  frfi  8751  iunfi  8800  indexfi  8820  supeq1  8897  supeq2  8900  bnd2  9310  acneq  9457  aceq3lem  9534  dfac5lem4  9540  dfac8  9549  dfac9  9550  kmlem1  9564  kmlem10  9573  kmlem13  9576  cfval  9657  axcc2lem  9846  axcc4dom  9851  axdc3lem3  9862  axdc3lem4  9863  ac4c  9886  ac5  9887  ac6sg  9898  zorn2lem7  9912  xrsupsslem  12688  xrinfmsslem  12689  xrsupss  12690  xrinfmss  12691  fsuppmapnn0fiubex  13348  rexanuz  14693  rexfiuz  14695  modfsummod  15137  gcdcllem3  15838  lcmfval  15953  lcmf0val  15954  lcmfunsnlem  15973  coprmprod  15993  coprmproddvds  15995  isprs  17528  drsdirfi  17536  isdrs2  17537  ispos  17545  lubeldm  17579  lubval  17582  glbeldm  17592  glbval  17595  istos  17633  pospropd  17732  isdlat  17791  mhmpropd  17950  isghm  18296  cntzval  18389  efgval  18772  iscmn  18843  dfrhm2  19398  lidldvgen  19956  coe1fzgsumd  20398  evl1gsumd  20448  ocvval  20739  isobs  20792  mat0dimcrng  21007  mdetunilem9  21157  ist0  21856  cmpcovf  21927  is1stc  21977  2ndc1stc  21987  isref  22045  txflf  22542  ustuqtop4  22780  iscfilu  22824  ispsmet  22841  ismet  22860  isxmet  22861  cncfval  23423  lebnumlem3  23494  fmcfil  23802  iscfil3  23803  caucfil  23813  iscmet3  23823  cfilres  23826  minveclem3  23959  ovolfiniun  24029  finiunmbl  24072  volfiniun  24075  dvcn  24445  ulmval  24895  axtgcont1  26181  nb3grpr  27091  dfconngr1  27894  isconngr  27895  1conngr  27900  frgr0v  27968  isplig  28180  isgrpo  28201  isablo  28250  ocval  28984  acunirnmpt  30332  isomnd  30629  isorng  30799  prmidl  30876  ismbfm  31409  isanmbfm  31413  bnj865  32094  bnj1154  32168  bnj1296  32190  bnj1463  32224  derangval  32311  setinds  32920  dfon2lem3  32927  dfon2lem7  32931  tfisg  32952  poseq  32992  frrlem1  33020  frrlem13  33032  sltval2  33060  sltres  33066  nolesgn2o  33075  nodense  33093  nosupbnd2lem1  33112  brsslt  33151  dfrecs2  33308  dfrdg4  33309  isfne  33584  finixpnum  34758  mblfinlem1  34810  mbfresfi  34819  indexdom  34890  heibor1lem  34968  isexid2  35014  ismndo2  35033  rngomndo  35094  pridl  35196  smprngopr  35211  ispridlc  35229  setindtrs  39500  dford3lem2  39502  dfac11  39540  mnuop123d  40475  fnchoice  41163  axccdom  41363  axccd  41371  stoweidlem31  42193  stoweidlem57  42219  fourierdlem80  42348  fourierdlem103  42371  fourierdlem104  42372  isvonmbl  42797  paireqne  43550  requad2  43665  mgmhmpropd  43929  rnghmval  44090  zrrnghm  44116  bnd2d  44712
  Copyright terms: Public domain W3C validator