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

Theorem raleqi 2868
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 2864 . 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 177    = wceq 1649   A.wral 2666
This theorem is referenced by:  ralrab2  3060  ralprg  3817  raltpg  3819  ralxp  4975  ralrnmpt2  6143  ovmptss  6387  ixpfi2  7363  dffi3  7394  dfoi  7436  fseqenlem1  7861  kmlem12  7997  fzprval  11062  fztpval  11063  hashbc  11657  2prm  13050  prmreclem2  13240  xpsfrnel  13743  xpsle  13761  gsumwspan  14746  basdif0  16973  ordtbaslem  17206  ptbasfi  17566  ptcnplem  17606  ptrescn  17624  flftg  17981  ust0  18202  minveclem1  19278  minveclem3b  19282  minveclem6  19288  iblcnlem1  19632  ellimc2  19717  ftalem3  20810  dchreq  20995  pntlem3  21256  cusgra3v  21426  cusgrares  21434  0wlk  21498  0trl  21499  wlkntrllem2  21513  usgrcyclnl2  21581  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv4e  21608  elghom  21904  minvecolem1  22329  minvecolem5  22336  minvecolem6  22337  cdj3lem3b  23896  prsiga  24467  hfext  26028  filnetlem4  26300  iscrngo2  26498  fnwe2lem2  27016  islinds2  27151  psgnunilem3  27287  f12dfv  27961  f13dfv  27962  usgra2pthspth  28035  usgra2pthlem1  28040  tendoset  31241
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671
  Copyright terms: Public domain W3C validator