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

Theorem ralbiia 2651
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 2647 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 1710   A.wral 2619
This theorem is referenced by:  reusv7OLD  4625  poinxp  4832  soinxp  4833  seinxp  4835  dffun8  5360  funcnv3  5390  fncnv  5393  fnres  5439  fvreseq  5708  isoini2  5920  smores  6453  resixp  6936  ixpfi2  7241  marypha1lem  7273  ac5num  7750  acni2  7760  acndom  7765  dfac4  7836  brdom7disj  8243  brdom6disj  8244  fpwwe2lem8  8346  axgroth6  8537  lo1res  12123  isprm5  12882  prmreclem2  13055  tsrss  14425  gass  14848  efgval2  15126  efgsres  15140  isdomn2  16133  isclo  16924  ptclsg  17409  ufilcmp  17823  cfilres  18820  ovolgelb  18937  volsup2  19058  vitali  19066  itg1climres  19167  itg2seq  19195  itg2monolem1  19203  itg2mono  19206  itg2i1fseq  19208  itg2cn  19216  ellimc2  19325  rolle  19435  lhop1  19459  itgsubstlem  19493  tdeglem4  19544  dvdsmulf1o  20540  dchrelbas2  20582  selbergsb  20830  hodsi  22463  ho01i  22516  ho02i  22517  lnopeqi  22696  nmcopexi  22715  nmcfnexi  22739  cnlnadjlem3  22757  cnlnadjlem5  22759  leop3  22813  pjssposi  22860  largei  22955  mdsl2i  23010  mdsl2bi  23011  elat2  23028  dmdbr5ati  23110  cdj3lem3b  23128  subfacp1lem3  24117  dfso3  24478  tfr3ALT  24837  axcontlem2  25152  voliunnfl  25490  islinds2  26606  acsfn1p  26830  dfconngra1  27778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557
This theorem depends on definitions:  df-bi 177  df-ral 2624
  Copyright terms: Public domain W3C validator