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

Theorem raleqi 3115
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 3111 . 2 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
31, 2ax-mp 5 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wral 2892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897
This theorem is referenced by:  ralrab2  3335  ralprg  4177  raltpg  4179  ralxp  5170  f12dfv  6404  f13dfv  6405  ralrnmpt2  6648  ovmptss  7119  ixpfi2  8121  dffi3  8194  dfoi  8273  fseqenlem1  8704  kmlem12  8840  fzprval  12223  fztpval  12224  hashbc  13043  2prm  15186  prmreclem2  15402  xpsfrnel  15989  xpsle  16007  gsumwspan  17149  sgrp2rid2  17179  psgnunilem3  17682  pmtrsn  17705  ply1coe  19430  cply1coe0bi  19434  islinds2  19910  m2cpminvid2lem  20317  basdif0  20507  ordtbaslem  20741  ptbasfi  21133  ptcnplem  21173  ptrescn  21191  flftg  21549  ust0  21772  minveclem1  22917  minveclem3b  22921  minveclem6  22927  iblcnlem1  23274  ellimc2  23361  ftalem3  24515  dchreq  24697  pntlem3  25012  istrkg2ld  25073  istrkg3ld  25074  cusgra3v  25756  cusgrares  25764  0wlk  25838  0trl  25839  wlkntrllem2  25853  usgrcyclnl2  25932  3v3e3cycl1  25935  4cycl4v4e  25957  4cycl4dv4e  25959  rusgranumwlkl1  26237  minvecolem1  26917  minvecolem5  26924  minvecolem6  26925  cdj3lem3b  28486  prsiga  29324  hfext  31263  filnetlem4  31349  relowlssretop  32187  relowlpssretop  32188  elghomOLD  32656  iscrngo2  32766  tendoset  34865  fnwe2lem2  36439  eliuniincex  38123  eliincex  38124  subsaliuncl  39053  lfuhgr1v0e  40479  cplgr0  40646  1wlkp1lem8  40888  usgr2pthlem  40968  pthdlem1  40971  pthd  40974  crctcsh1wlkn0  41023  21wlkdlem4  41134  21wlkdlem5  41135  2pthdlem1  41136  21wlkdlem10  41141  rusgrnumwwlkl1  41171  0ewlk  41281  01wlk  41283  1wlk2v2elem2  41322  31wlkdlem4  41328  31wlkdlem5  41329  3pthdlem1  41330  31wlkdlem10  41335
  Copyright terms: Public domain W3C validator