Theorem ralbiia 2887

Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)

Hypothesis

Ref	Expression
ralbiia.1

Assertion

Ref	Expression
ralbiia

Proof of Theorem ralbiia

Step	Hyp	Ref	Expression
1		ralbiia.1	. . 3
2	1	pm5.74i 245	. 2
3	2	ralbii2 2886	1

Syntax hints:  ->wi 4  <->wb 184  e.wcel 1818  A.wral 2807

This theorem is referenced by:  reusv7OLD  4664  poinxp  5068  soinxp  5069  seinxp  5071  dffun8  5620  funcnv3  5654  fncnv  5657  fnres  5702  fvreseq0  5987  isoini2  6235  smores  7042  resixp  7524  ixpfi2  7838  marypha1lem  7913  ac5num  8438  acni2  8448  acndom  8453  dfac4  8524  brdom7disj  8930  brdom6disj  8931  fpwwe2lem8  9036  axgroth6  9227  rabssnn0fi  12095  lo1res  13382  isprm5  14253  prmreclem2  14435  tsrss  15853  gass  16339  efgval2  16742  efgsres  16756  isdomn2  17948  islinds2  18848  isclo  19588  ptclsg  20116  ufilcmp  20533  cfilres  21735  ovolgelb  21891  volsup2  22014  vitali  22022  itg1climres  22121  itg2seq  22149  itg2monolem1  22157  itg2mono  22160  itg2i1fseq  22162  itg2cn  22170  ellimc2  22281  rolle  22391  lhop1  22415  itgsubstlem  22449  tdeglem4  22458  dvdsmulf1o  23470  dchrelbas2  23512  selbergsb  23760  axcontlem2  24268  dfconngra1  24671  hodsi  26694  ho01i  26747  ho02i  26748  lnopeqi  26927  nmcopexi  26946  nmcfnexi  26970  cnlnadjlem3  26988  cnlnadjlem5  26990  leop3  27044  pjssposi  27091  largei  27186  mdsl2i  27241  mdsl2bi  27242  elat2  27259  dmdbr5ati  27341  cdj3lem3b  27359  subfacp1lem3  28626  dfso3  29097  tfr3ALT  29365  mblfinlem1  30051  voliunnfl  30058  acsfn1p  31148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631

This theorem depends on definitions:  df-bi 185  df-ral 2812