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

Theorem ralbiia 2768
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 245 . 2  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  ->  ps )
)
32ralbii2 2764 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    e. wcel 1756   A.wral 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-ral 2741
This theorem is referenced by:  reusv7OLD  4525  poinxp  4923  soinxp  4924  seinxp  4926  dffun8  5466  funcnv3  5500  fncnv  5503  fnres  5548  fvreseq0  5824  isoini2  6051  smores  6834  resixp  7319  ixpfi2  7630  marypha1lem  7704  ac5num  8227  acni2  8237  acndom  8242  dfac4  8313  brdom7disj  8719  brdom6disj  8720  fpwwe2lem8  8825  axgroth6  9016  lo1res  13058  isprm5  13819  prmreclem2  13999  tsrss  15414  gass  15840  efgval2  16242  efgsres  16256  isdomn2  17393  islinds2  18264  isclo  18713  ptclsg  19210  ufilcmp  19627  cfilres  20829  ovolgelb  20985  volsup2  21107  vitali  21115  itg1climres  21214  itg2seq  21242  itg2monolem1  21250  itg2mono  21253  itg2i1fseq  21255  itg2cn  21263  ellimc2  21374  rolle  21484  lhop1  21508  itgsubstlem  21542  tdeglem4  21551  dvdsmulf1o  22556  dchrelbas2  22598  selbergsb  22846  axcontlem2  23233  dfconngra1  23579  hodsi  25201  ho01i  25254  ho02i  25255  lnopeqi  25434  nmcopexi  25453  nmcfnexi  25477  cnlnadjlem3  25495  cnlnadjlem5  25497  leop3  25551  pjssposi  25598  largei  25693  mdsl2i  25748  mdsl2bi  25749  elat2  25766  dmdbr5ati  25848  cdj3lem3b  25866  subfacp1lem3  27092  dfso3  27398  tfr3ALT  27768  mblfinlem1  28454  voliunnfl  28461  acsfn1p  29582  rabssnn0fi  30776
  Copyright terms: Public domain W3C validator