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

Theorem ralbiia 2698
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 237 . 2  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  ->  ps )
)
32ralbii2 2694 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    e. wcel 1721   A.wral 2666
This theorem is referenced by:  reusv7OLD  4694  poinxp  4900  soinxp  4901  seinxp  4903  dffun8  5439  funcnv3  5471  fncnv  5474  fnres  5520  fvreseq  5792  isoini2  6018  smores  6573  resixp  7056  ixpfi2  7363  marypha1lem  7396  ac5num  7873  acni2  7883  acndom  7888  dfac4  7959  brdom7disj  8365  brdom6disj  8366  fpwwe2lem8  8468  axgroth6  8659  lo1res  12308  isprm5  13067  prmreclem2  13240  tsrss  14610  gass  15033  efgval2  15311  efgsres  15325  isdomn2  16314  isclo  17106  ptclsg  17600  ufilcmp  18017  cfilres  19202  ovolgelb  19329  volsup2  19450  vitali  19458  itg1climres  19559  itg2seq  19587  itg2monolem1  19595  itg2mono  19598  itg2i1fseq  19600  itg2cn  19608  ellimc2  19717  rolle  19827  lhop1  19851  itgsubstlem  19885  tdeglem4  19936  dvdsmulf1o  20932  dchrelbas2  20974  selbergsb  21222  dfconngra1  21611  hodsi  23231  ho01i  23284  ho02i  23285  lnopeqi  23464  nmcopexi  23483  nmcfnexi  23507  cnlnadjlem3  23525  cnlnadjlem5  23527  leop3  23581  pjssposi  23628  largei  23723  mdsl2i  23778  mdsl2bi  23779  elat2  23796  dmdbr5ati  23878  cdj3lem3b  23896  subfacp1lem3  24821  dfso3  25130  tfr3ALT  25493  axcontlem2  25808  mblfinlem  26143  voliunnfl  26149  islinds2  27151  acsfn1p  27375
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-ral 2671
  Copyright terms: Public domain W3C validator