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

Theorem raleqi 3029
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 3025 . 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 187    = wceq 1437   A.wral 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780
This theorem is referenced by:  ralrab2  3237  ralprg  4046  raltpg  4048  ralxp  4992  f12dfv  6184  f13dfv  6185  ralrnmpt2  6422  ovmptss  6885  ixpfi2  7875  dffi3  7948  dfoi  8029  fseqenlem1  8456  kmlem12  8592  fzprval  11857  fztpval  11858  hashbc  12614  2prm  14628  prmreclem2  14849  xpsfrnel  15457  xpsle  15475  gsumwspan  16618  sgrp2rid2  16648  psgnunilem3  17125  pmtrsn  17148  ply1coe  18877  cply1coe0bi  18882  islinds2  19358  m2cpminvid2lem  19765  basdif0  19955  ordtbaslem  20191  ptbasfi  20583  ptcnplem  20623  ptrescn  20641  flftg  20998  ust0  21221  minveclem1  22353  minveclem3b  22357  minveclem6  22363  minveclem3bOLD  22369  minveclem6OLD  22375  iblcnlem1  22732  ellimc2  22819  ftalem3  23986  dchreq  24173  pntlem3  24434  istrkg2ld  24495  istrkg3ld  24496  cusgra3v  25178  cusgrares  25186  0wlk  25261  0trl  25262  wlkntrllem2  25276  usgrcyclnl2  25355  3v3e3cycl1  25358  4cycl4v4e  25380  4cycl4dv4e  25382  rusgranumwlkl1  25661  elghomOLD  26077  minvecolem1  26502  minvecolem5  26509  minvecolem6  26510  minvecolem5OLD  26519  minvecolem6OLD  26520  cdj3lem3b  28079  prsiga  28949  hfext  30943  filnetlem4  31030  relowlssretop  31707  relowlpssretop  31708  iscrngo2  32145  tendoset  34245  fnwe2lem2  35829  usgra2pthspth  38937  usgra2pthlem1  38939
  Copyright terms: Public domain W3C validator