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

Theorem raleqi 2919
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 2915 . 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 1364   A.wral 2713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718
This theorem is referenced by:  ralrab2  3122  ralprg  3922  raltpg  3924  ralxp  4977  ralrnmpt2  6204  ovmptss  6653  ixpfi2  7605  dffi3  7677  dfoi  7721  fseqenlem1  8190  kmlem12  8326  fzprval  11513  fztpval  11514  hashbc  12202  2prm  13775  prmreclem2  13974  xpsfrnel  14497  xpsle  14515  gsumwspan  15517  psgnunilem3  15995  islinds2  18201  basdif0  18517  ordtbaslem  18751  ptbasfi  19113  ptcnplem  19153  ptrescn  19171  flftg  19528  ust0  19753  minveclem1  20870  minveclem3b  20874  minveclem6  20880  iblcnlem1  21224  ellimc2  21311  ftalem3  22371  dchreq  22556  pntlem3  22817  cusgra3v  23307  cusgrares  23315  0wlk  23379  0trl  23380  wlkntrllem2  23394  usgrcyclnl2  23462  3v3e3cycl1  23465  4cycl4v4e  23487  4cycl4dv4e  23489  elghom  23785  minvecolem1  24210  minvecolem5  24217  minvecolem6  24218  cdj3lem3b  25779  prsiga  26510  hfext  28150  filnetlem4  28527  iscrngo2  28723  fnwe2lem2  29329  f12dfv  30071  f13dfv  30072  usgra2pthspth  30220  usgra2pthlem1  30225  rusgranumwlkl1  30484  pmtrsn  30687  tendoset  34125
  Copyright terms: Public domain W3C validator