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

Theorem raleqi 3413
Description: Equality inference for restricted universal quantifier. (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 3405 . 2 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
31, 2ax-mp 5 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 208   = wceq 1533  wral 3138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-ral 3143
This theorem is referenced by:  ralrab2  3689  ralprgf  4629  raltpg  4633  ralxp  5711  f12dfv  7029  f13dfv  7030  ralrnmpo  7288  ovmptss  7787  ixpfi2  8821  dffi3  8894  dfoi  8974  fseqenlem1  9449  kmlem12  9586  fzprval  12967  fztpval  12968  hashbc  13810  2prm  16035  prmreclem2  16252  xpsfrnel  16834  xpsle  16851  gsumwspan  18010  sgrp2rid2  18090  psgnunilem3  18623  pmtrsn  18646  ply1coe  20463  cply1coe0bi  20467  islinds2  20956  m2cpminvid2lem  21361  basdif0  21560  ordtbaslem  21795  ptbasfi  22188  ptcnplem  22228  ptrescn  22246  flftg  22603  ust0  22827  minveclem1  24026  minveclem3b  24030  minveclem6  24036  iblcnlem1  24387  ellimc2  24474  ftalem3  25651  dchreq  25833  pntlem3  26184  istrkg2ld  26245  istrkg3ld  26246  tgcgr4  26316  elntg2  26770  lfuhgr1v0e  27035  cplgr0  27206  wlkp1lem8  27461  usgr2pthlem  27543  pthdlem1  27546  pthd  27549  crctcshwlkn0  27598  2wlkdlem4  27706  2wlkdlem5  27707  2pthdlem1  27708  2wlkdlem10  27713  rusgrnumwwlkl1  27746  0ewlk  27892  0wlk  27894  wlk2v2elem2  27934  3wlkdlem4  27940  3wlkdlem5  27941  3pthdlem1  27942  3wlkdlem10  27947  minvecolem1  28650  minvecolem5  28657  minvecolem6  28658  cdj3lem3b  30216  prsiga  31390  hfext  33644  filnetlem4  33729  relowlssretop  34643  relowlpssretop  34644  elghomOLD  35164  iscrngo2  35274  refrelcoss3  35702  tendoset  37894  fnwe2lem2  39649  eliuniincex  41373  eliincex  41374  uzub  41703  liminflelimsuplem  42054  xlimbr  42106  subsaliuncl  42640  isomushgr  43990  rrx2pnecoorneor  44701  rrx2linest  44728
  Copyright terms: Public domain W3C validator