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

Theorem raleqi 3062
Description: Equality inference for restricted universal qualifier. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
raleq1i.1  |-  A  =  B
Assertion
Ref Expression
raleqi  |-  ( A. x  e.  A  ph  <->  A. x  e.  B  ph )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem raleqi
StepHypRef Expression
1 raleq1i.1 . 2  |-  A  =  B
2 raleq 3058 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
31, 2ax-mp 5 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  B  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1379   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819
This theorem is referenced by:  ralrab2  3269  ralprg  4076  raltpg  4078  ralxp  5143  f12dfv  6166  f13dfv  6167  ralrnmpt2  6400  ovmptss  6864  ixpfi2  7817  dffi3  7890  dfoi  7935  fseqenlem1  8404  kmlem12  8540  fzprval  11739  fztpval  11740  hashbc  12467  2prm  14091  prmreclem2  14293  xpsfrnel  14817  xpsle  14835  gsumwspan  15843  psgnunilem3  16324  pmtrsn  16347  ply1coe  18124  cply1coe0bi  18129  islinds2  18631  m2cpminvid2lem  19038  basdif0  19237  ordtbaslem  19471  ptbasfi  19833  ptcnplem  19873  ptrescn  19891  flftg  20248  ust0  20473  minveclem1  21590  minveclem3b  21594  minveclem6  21600  iblcnlem1  21945  ellimc2  22032  ftalem3  23092  dchreq  23277  pntlem3  23538  istrkg2ld  23602  cusgra3v  24156  cusgrares  24164  0wlk  24239  0trl  24240  wlkntrllem2  24254  usgrcyclnl2  24333  3v3e3cycl1  24336  4cycl4v4e  24358  4cycl4dv4e  24360  rusgranumwlkl1  24639  elghom  25057  minvecolem1  25482  minvecolem5  25489  minvecolem6  25490  cdj3lem3b  27051  prsiga  27787  hfext  29433  filnetlem4  29818  iscrngo2  30014  fnwe2lem2  30617  usgra2pthspth  31834  usgra2pthlem1  31836  tendoset  35564
  Copyright terms: Public domain W3C validator