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

Theorem ralbiia 2862
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 248 . 2  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  ->  ps )
)
32ralbii2 2861 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    e. wcel 1870   A.wral 2782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-ral 2787
This theorem is referenced by:  poinxp  4918  soinxp  4919  seinxp  4921  dffun8  5628  funcnv3  5662  fncnv  5665  fnres  5710  fvreseq0  5997  isoini2  6245  smores  7079  tfr3ALT  7128  resixp  7565  ixpfi2  7878  marypha1lem  7953  ac5num  8465  acni2  8475  acndom  8480  dfac4  8551  brdom7disj  8957  brdom6disj  8958  fpwwe2lem8  9061  axgroth6  9252  rabssnn0fi  12195  lo1res  13601  isprm5  14622  prmreclem2  14824  tsrss  16420  gass  16906  efgval2  17309  efgsres  17323  isdomn2  18458  islinds2  19302  isclo  20034  ptclsg  20561  ufilcmp  20978  cfilres  22159  ovolgelb  22311  volsup2  22440  vitali  22448  itg1climres  22549  itg2seq  22577  itg2monolem1  22585  itg2mono  22588  itg2i1fseq  22590  itg2cn  22598  ellimc2  22709  rolle  22819  lhop1  22843  itgsubstlem  22877  tdeglem4  22886  dvdsmulf1o  23986  dchrelbas2  24028  selbergsb  24276  axcontlem2  24841  dfconngra1  25244  hodsi  27263  ho01i  27316  ho02i  27317  lnopeqi  27496  nmcopexi  27515  nmcfnexi  27539  cnlnadjlem3  27557  cnlnadjlem5  27559  leop3  27613  pjssposi  27660  largei  27755  mdsl2i  27810  mdsl2bi  27811  elat2  27828  dmdbr5ati  27910  cdj3lem3b  27928  subfacp1lem3  29693  dfso3  30140  phpreu  31633  ptrecube  31644  mblfinlem1  31681  voliunnfl  31688  acsfn1p  35764  sgoldbalt  38272
  Copyright terms: Public domain W3C validator