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

Theorem raleqi 3135
Description: Equality inference for restricted universal qualifier. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
raleq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
raleqi (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleqi
StepHypRef Expression
1 raleq1i.1 . 2 𝐴 = 𝐵
2 raleq 3131 . 2 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
31, 2ax-mp 5 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1480  wral 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913
This theorem is referenced by:  ralrab2  3359  ralprg  4212  raltpg  4214  ralxp  5233  f12dfv  6494  f13dfv  6495  ralrnmpt2  6740  ovmptss  7218  ixpfi2  8224  dffi3  8297  dfoi  8376  fseqenlem1  8807  kmlem12  8943  fzprval  12359  fztpval  12360  hashbc  13191  2prm  15348  prmreclem2  15564  xpsfrnel  16163  xpsle  16181  gsumwspan  17323  sgrp2rid2  17353  psgnunilem3  17856  pmtrsn  17879  ply1coe  19606  cply1coe0bi  19610  islinds2  20092  m2cpminvid2lem  20499  basdif0  20697  ordtbaslem  20932  ptbasfi  21324  ptcnplem  21364  ptrescn  21382  flftg  21740  ust0  21963  minveclem1  23135  minveclem3b  23139  minveclem6  23145  iblcnlem1  23494  ellimc2  23581  ftalem3  24735  dchreq  24917  pntlem3  25232  istrkg2ld  25293  istrkg3ld  25294  lfuhgr1v0e  26073  cplgr0  26242  wlkp1lem8  26480  usgr2pthlem  26562  pthdlem1  26565  pthd  26568  crctcshwlkn0  26616  2wlkdlem4  26727  2wlkdlem5  26728  2pthdlem1  26729  2wlkdlem10  26734  rusgrnumwwlkl1  26764  0ewlk  26875  0wlk  26877  wlk2v2elem2  26916  3wlkdlem4  26922  3wlkdlem5  26923  3pthdlem1  26924  3wlkdlem10  26929  minvecolem1  27618  minvecolem5  27625  minvecolem6  27626  cdj3lem3b  29187  prsiga  30017  hfext  31985  filnetlem4  32071  relowlssretop  32882  relowlpssretop  32883  elghomOLD  33357  iscrngo2  33467  tendoset  35566  fnwe2lem2  37140  eliuniincex  38816  eliincex  38817  uzub  39157  subsaliuncl  39913
  Copyright terms: Public domain W3C validator