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

Theorem raleqi 2852
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 2848 . 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 2650
This theorem is referenced by:  ralrab2  3044  ralprg  3801  raltpg  3803  ralxp  4957  ralrnmpt2  6124  ovmptss  6368  ixpfi2  7341  dffi3  7372  dfoi  7414  fseqenlem1  7839  kmlem12  7975  fzprval  11038  fztpval  11039  hashbc  11630  2prm  13023  prmreclem2  13213  xpsfrnel  13716  xpsle  13734  gsumwspan  14719  basdif0  16942  ordtbaslem  17175  ptbasfi  17535  ptcnplem  17575  ptrescn  17593  flftg  17950  ust0  18171  minveclem1  19193  minveclem3b  19197  minveclem6  19203  iblcnlem1  19547  ellimc2  19632  ftalem3  20725  dchreq  20910  pntlem3  21171  cusgra3v  21340  cusgrares  21348  0wlk  21410  0trl  21411  wlkntrllem4  21417  usgrcyclnl2  21477  3v3e3cycl1  21480  4cycl4v4e  21502  4cycl4dv4e  21504  elghom  21800  minvecolem1  22225  minvecolem5  22232  minvecolem6  22233  cdj3lem3b  23792  prsiga  24311  hfext  25839  filnetlem4  26102  iscrngo2  26300  fnwe2lem2  26818  islinds2  26953  psgnunilem3  27089  tendoset  30874
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ral 2655
  Copyright terms: Public domain W3C validator