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

Theorem raleqi 2933
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 2929 . 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 1369   A.wral 2727
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2732
This theorem is referenced by:  ralrab2  3137  ralprg  3937  raltpg  3939  ralxp  4993  ralrnmpt2  6217  ovmptss  6666  ixpfi2  7621  dffi3  7693  dfoi  7737  fseqenlem1  8206  kmlem12  8342  fzprval  11529  fztpval  11530  hashbc  12218  2prm  13791  prmreclem2  13990  xpsfrnel  14513  xpsle  14531  gsumwspan  15536  psgnunilem3  16014  ply1coe  17758  islinds2  18254  basdif0  18570  ordtbaslem  18804  ptbasfi  19166  ptcnplem  19206  ptrescn  19224  flftg  19581  ust0  19806  minveclem1  20923  minveclem3b  20927  minveclem6  20933  iblcnlem1  21277  ellimc2  21364  ftalem3  22424  dchreq  22609  pntlem3  22870  cusgra3v  23384  cusgrares  23392  0wlk  23456  0trl  23457  wlkntrllem2  23471  usgrcyclnl2  23539  3v3e3cycl1  23542  4cycl4v4e  23564  4cycl4dv4e  23566  elghom  23862  minvecolem1  24287  minvecolem5  24294  minvecolem6  24295  cdj3lem3b  25856  prsiga  26586  hfext  28233  filnetlem4  28614  iscrngo2  28810  fnwe2lem2  29416  f12dfv  30158  f13dfv  30159  usgra2pthspth  30307  usgra2pthlem1  30312  rusgranumwlkl1  30571  pmtrsn  30782  tendoset  34415
  Copyright terms: Public domain W3C validator