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

Theorem ralbiia 2737
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 2733 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 1755   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605
This theorem depends on definitions:  df-bi 185  df-ral 2710
This theorem is referenced by:  reusv7OLD  4492  poinxp  4889  soinxp  4890  seinxp  4892  dffun8  5433  funcnv3  5467  fncnv  5470  fnres  5515  fvreseq0  5791  isoini2  6017  smores  6799  resixp  7286  ixpfi2  7597  marypha1lem  7671  ac5num  8194  acni2  8204  acndom  8209  dfac4  8280  brdom7disj  8686  brdom6disj  8687  fpwwe2lem8  8791  axgroth6  8982  lo1res  13020  isprm5  13780  prmreclem2  13960  tsrss  15375  gass  15798  efgval2  16200  efgsres  16214  isdomn2  17292  islinds2  18083  isclo  18532  ptclsg  19029  ufilcmp  19446  cfilres  20648  ovolgelb  20804  volsup2  20926  vitali  20934  itg1climres  21033  itg2seq  21061  itg2monolem1  21069  itg2mono  21072  itg2i1fseq  21074  itg2cn  21082  ellimc2  21193  rolle  21303  lhop1  21327  itgsubstlem  21361  tdeglem4  21413  dvdsmulf1o  22418  dchrelbas2  22460  selbergsb  22708  axcontlem2  23033  dfconngra1  23379  hodsi  25001  ho01i  25054  ho02i  25055  lnopeqi  25234  nmcopexi  25253  nmcfnexi  25277  cnlnadjlem3  25295  cnlnadjlem5  25297  leop3  25351  pjssposi  25398  largei  25493  mdsl2i  25548  mdsl2bi  25549  elat2  25566  dmdbr5ati  25648  cdj3lem3b  25666  subfacp1lem3  26917  dfso3  27222  tfr3ALT  27592  mblfinlem1  28269  voliunnfl  28276  acsfn1p  29398
  Copyright terms: Public domain W3C validator