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

Theorem raleqi 3055
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 3051 . 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 1398   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809
This theorem is referenced by:  ralrab2  3262  ralprg  4065  raltpg  4067  ralxp  5133  f12dfv  6154  f13dfv  6155  ralrnmpt2  6390  ovmptss  6854  ixpfi2  7810  dffi3  7883  dfoi  7928  fseqenlem1  8396  kmlem12  8532  fzprval  11744  fztpval  11745  hashbc  12486  2prm  14317  prmreclem2  14519  xpsfrnel  15052  xpsle  15070  gsumwspan  16213  sgrp2rid2  16243  psgnunilem3  16720  pmtrsn  16743  ply1coe  18532  cply1coe0bi  18537  islinds2  19015  m2cpminvid2lem  19422  basdif0  19621  ordtbaslem  19856  ptbasfi  20248  ptcnplem  20288  ptrescn  20306  flftg  20663  ust0  20888  minveclem1  22005  minveclem3b  22009  minveclem6  22015  iblcnlem1  22360  ellimc2  22447  ftalem3  23546  dchreq  23731  pntlem3  23992  istrkg2ld  24056  cusgra3v  24666  cusgrares  24674  0wlk  24749  0trl  24750  wlkntrllem2  24764  usgrcyclnl2  24843  3v3e3cycl1  24846  4cycl4v4e  24868  4cycl4dv4e  24870  rusgranumwlkl1  25149  elghomOLD  25563  minvecolem1  25988  minvecolem5  25995  minvecolem6  25996  cdj3lem3b  27557  prsiga  28361  hfext  30068  filnetlem4  30439  iscrngo2  30635  fnwe2lem2  31236  usgra2pthspth  32723  usgra2pthlem1  32725  tendoset  36882
  Copyright terms: Public domain W3C validator