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

Theorem ralbiia 2894
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 2893 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 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-ral 2819
This theorem is referenced by:  reusv7OLD  4659  poinxp  5063  soinxp  5064  seinxp  5066  dffun8  5615  funcnv3  5649  fncnv  5652  fnres  5697  fvreseq0  5981  isoini2  6223  smores  7023  resixp  7504  ixpfi2  7818  marypha1lem  7893  ac5num  8417  acni2  8427  acndom  8432  dfac4  8503  brdom7disj  8909  brdom6disj  8910  fpwwe2lem8  9015  axgroth6  9206  rabssnn0fi  12063  lo1res  13345  isprm5  14112  prmreclem2  14294  tsrss  15710  gass  16144  efgval2  16548  efgsres  16562  isdomn2  17747  islinds2  18643  isclo  19382  ptclsg  19879  ufilcmp  20296  cfilres  21498  ovolgelb  21654  volsup2  21777  vitali  21785  itg1climres  21884  itg2seq  21912  itg2monolem1  21920  itg2mono  21923  itg2i1fseq  21925  itg2cn  21933  ellimc2  22044  rolle  22154  lhop1  22178  itgsubstlem  22212  tdeglem4  22221  dvdsmulf1o  23226  dchrelbas2  23268  selbergsb  23516  axcontlem2  23972  dfconngra1  24375  hodsi  26398  ho01i  26451  ho02i  26452  lnopeqi  26631  nmcopexi  26650  nmcfnexi  26674  cnlnadjlem3  26692  cnlnadjlem5  26694  leop3  26748  pjssposi  26795  largei  26890  mdsl2i  26945  mdsl2bi  26946  elat2  26963  dmdbr5ati  27045  cdj3lem3b  27063  subfacp1lem3  28294  dfso3  28600  tfr3ALT  28970  mblfinlem1  29656  voliunnfl  29663  acsfn1p  30781
  Copyright terms: Public domain W3C validator