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

Theorem raleqi 2900
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 2896 . 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 1652   A.wral 2697
This theorem is referenced by:  ralrab2  3092  ralprg  3849  raltpg  3851  ralxp  5008  ralrnmpt2  6176  ovmptss  6420  ixpfi2  7397  dffi3  7428  dfoi  7472  fseqenlem1  7897  kmlem12  8033  fzprval  11098  fztpval  11099  hashbc  11694  2prm  13087  prmreclem2  13277  xpsfrnel  13780  xpsle  13798  gsumwspan  14783  basdif0  17010  ordtbaslem  17244  ptbasfi  17605  ptcnplem  17645  ptrescn  17663  flftg  18020  ust0  18241  minveclem1  19317  minveclem3b  19321  minveclem6  19327  iblcnlem1  19671  ellimc2  19756  ftalem3  20849  dchreq  21034  pntlem3  21295  cusgra3v  21465  cusgrares  21473  0wlk  21537  0trl  21538  wlkntrllem2  21552  usgrcyclnl2  21620  3v3e3cycl1  21623  4cycl4v4e  21645  4cycl4dv4e  21647  elghom  21943  minvecolem1  22368  minvecolem5  22375  minvecolem6  22376  cdj3lem3b  23935  prsiga  24506  hfext  26116  filnetlem4  26391  iscrngo2  26589  fnwe2lem2  27107  islinds2  27241  psgnunilem3  27377  f12dfv  28056  f13dfv  28057  usgra2pthspth  28248  usgra2pthlem1  28253  tendoset  31483
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702
  Copyright terms: Public domain W3C validator