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

Theorem raleqi 2753
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 2749 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
31, 2ax-mp 8 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  B  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1632   A.wral 2556
This theorem is referenced by:  ralrab2  2944  ralprg  3695  raltpg  3697  ralxp  4843  ralrnmpt2  5974  ovmptss  6216  ixpfi2  7170  dffi3  7200  dfoi  7242  fseqenlem1  7667  kmlem12  7803  fzprval  10860  fztpval  10861  hashbc  11407  2prm  12790  prmreclem2  12980  xpsfrnel  13481  xpsle  13499  gsumwspan  14484  basdif0  16707  ordtbaslem  16934  ptbasfi  17292  ptcnplem  17331  ptrescn  17349  flftg  17707  minveclem1  18804  minveclem3b  18808  minveclem6  18814  iblcnlem1  19158  ellimc2  19243  ftalem3  20328  dchreq  20513  pntlem3  20774  elghom  21046  minvecolem1  21469  minvecolem5  21476  minvecolem6  21477  cdj3lem3b  23036  cnvref  25168  repcpwti  25264  filnetlem4  26433  iscrngo2  26726  fnwe2lem2  27251  islinds2  27386  psgnunilem3  27522  cusgra3v  28299  0wlk  28343  0trl  28344  wlkntrllem4  28348  usgrcyclnl2  28387  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv4e  28414  tendoset  31570
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561
  Copyright terms: Public domain W3C validator