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

Theorem raleqi 3119
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 3115 . 2 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
31, 2ax-mp 5 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 195   = wceq 1475  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901
This theorem is referenced by:  ralrab2  3339  ralprg  4181  raltpg  4183  ralxp  5185  f12dfv  6429  f13dfv  6430  ralrnmpt2  6673  ovmptss  7145  ixpfi2  8147  dffi3  8220  dfoi  8299  fseqenlem1  8730  kmlem12  8866  fzprval  12271  fztpval  12272  hashbc  13094  2prm  15243  prmreclem2  15459  xpsfrnel  16046  xpsle  16064  gsumwspan  17206  sgrp2rid2  17236  psgnunilem3  17739  pmtrsn  17762  ply1coe  19487  cply1coe0bi  19491  islinds2  19971  m2cpminvid2lem  20378  basdif0  20568  ordtbaslem  20802  ptbasfi  21194  ptcnplem  21234  ptrescn  21252  flftg  21610  ust0  21833  minveclem1  23003  minveclem3b  23007  minveclem6  23013  iblcnlem1  23360  ellimc2  23447  ftalem3  24601  dchreq  24783  pntlem3  25098  istrkg2ld  25159  istrkg3ld  25160  cusgra3v  25993  cusgrares  26001  0wlk  26075  0trl  26076  wlkntrllem2  26090  usgrcyclnl2  26169  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  rusgranumwlkl1  26474  minvecolem1  27114  minvecolem5  27121  minvecolem6  27122  cdj3lem3b  28683  prsiga  29521  hfext  31460  filnetlem4  31546  relowlssretop  32387  relowlpssretop  32388  elghomOLD  32856  iscrngo2  32966  tendoset  35065  fnwe2lem2  36639  eliuniincex  38323  eliincex  38324  subsaliuncl  39252  lfuhgr1v0e  40480  cplgr0  40647  1wlkp1lem8  40889  usgr2pthlem  40969  pthdlem1  40972  pthd  40975  crctcsh1wlkn0  41024  21wlkdlem4  41135  21wlkdlem5  41136  2pthdlem1  41137  21wlkdlem10  41142  rusgrnumwwlkl1  41172  0ewlk  41282  01wlk  41284  1wlk2v2elem2  41323  31wlkdlem4  41329  31wlkdlem5  41330  3pthdlem1  41331  31wlkdlem10  41336
  Copyright terms: Public domain W3C validator