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

Theorem ralbiia 2575
Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)
Hypothesis
Ref Expression
ralbiia.1  |-  ( x  e.  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
ralbiia  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )

Proof of Theorem ralbiia
StepHypRef Expression
1 ralbiia.1 . . 3  |-  ( x  e.  A  ->  ( ph 
<->  ps ) )
21pm5.74i 236 . 2  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  ->  ps )
)
32ralbii2 2571 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    e. wcel 1684   A.wral 2543
This theorem is referenced by:  reusv7OLD  4546  poinxp  4753  soinxp  4754  seinxp  4756  dffun8  5281  funcnv3  5311  fncnv  5314  fnres  5360  fvreseq  5628  isoini2  5836  smores  6369  resixp  6851  ixpfi2  7154  marypha1lem  7186  ac5num  7663  acni2  7673  acndom  7678  dfac4  7749  brdom7disj  8156  brdom6disj  8157  fpwwe2lem8  8259  axgroth6  8450  lo1res  12033  isprm5  12791  prmreclem2  12964  tsrss  14332  gass  14755  efgval2  15033  efgsres  15047  isdomn2  16040  isclo  16824  ptclsg  17309  ufilcmp  17727  cfilres  18722  ovolgelb  18839  volsup2  18960  vitali  18968  itg1climres  19069  itg2seq  19097  itg2monolem1  19105  itg2mono  19108  itg2i1fseq  19110  itg2cn  19118  ellimc2  19227  rolle  19337  lhop1  19361  itgsubstlem  19395  tdeglem4  19446  dvdsmulf1o  20434  dchrelbas2  20476  selbergsb  20724  hodsi  22355  ho01i  22408  ho02i  22409  lnopeqi  22588  nmcopexi  22607  nmcfnexi  22631  cnlnadjlem3  22649  cnlnadjlem5  22651  leop3  22705  pjssposi  22752  largei  22847  mdsl2i  22902  mdsl2bi  22903  elat2  22920  dmdbr5ati  23002  cdj3lem3b  23020  subfacp1lem3  23713  dfso3  24074  tfr3ALT  24279  axcontlem2  24593  cnvref  25065  svli2  25484  islinds2  27283  acsfn1p  27507
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ral 2548
  Copyright terms: Public domain W3C validator