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

Theorem ralbiia 2739
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 238 . 2  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  ->  ps )
)
32ralbii2 2735 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    e. wcel 1726   A.wral 2707
This theorem is referenced by:  reusv7OLD  4738  poinxp  4944  soinxp  4945  seinxp  4947  dffun8  5483  funcnv3  5515  fncnv  5518  fnres  5564  fvreseq  5836  isoini2  6062  smores  6617  resixp  7100  ixpfi2  7408  marypha1lem  7441  ac5num  7922  acni2  7932  acndom  7937  dfac4  8008  brdom7disj  8414  brdom6disj  8415  fpwwe2lem8  8517  axgroth6  8708  lo1res  12358  isprm5  13117  prmreclem2  13290  tsrss  14660  gass  15083  efgval2  15361  efgsres  15375  isdomn2  16364  isclo  17156  ptclsg  17652  ufilcmp  18069  cfilres  19254  ovolgelb  19381  volsup2  19502  vitali  19510  itg1climres  19609  itg2seq  19637  itg2monolem1  19645  itg2mono  19648  itg2i1fseq  19650  itg2cn  19658  ellimc2  19769  rolle  19879  lhop1  19903  itgsubstlem  19937  tdeglem4  19988  dvdsmulf1o  20984  dchrelbas2  21026  selbergsb  21274  dfconngra1  21663  hodsi  23283  ho01i  23336  ho02i  23337  lnopeqi  23516  nmcopexi  23535  nmcfnexi  23559  cnlnadjlem3  23577  cnlnadjlem5  23579  leop3  23633  pjssposi  23680  largei  23775  mdsl2i  23830  mdsl2bi  23831  elat2  23848  dmdbr5ati  23930  cdj3lem3b  23948  subfacp1lem3  24873  dfso3  25182  tfr3ALT  25565  axcontlem2  25909  mblfinlem1  26255  voliunnfl  26262  islinds2  27274  acsfn1p  27498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-ral 2712
  Copyright terms: Public domain W3C validator