Theorem ralbiia 2491

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

Step	Hyp	Ref	Expression
1		ralbiia.1	. . 3 |- ( x e. A -> ( ph <-> ps ) )
2	1	pm5.74i 180	. 2 |- ( ( x e. A -> ph ) <-> ( x e. A -> ps ) )
3	2	ralbii2 2487	1 |- ( A. x e. A ph <-> A. x e. A ps )

Syntax hints:   -> wi 4   <-> wb 105   e. wcel 2148   A.wral 2455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449

This theorem depends on definitions:  df-bi 117  df-ral 2460

This theorem is referenced by:  frind  4352  poinxp  4695  soinxp  4696  seinxp  4697  dffun8  5244  funcnv3  5278  fncnv  5282  fnres  5332  fvreseq  5619  isoini2  5819  smores  6292  resixp  6732  pw1dc1  6912  finomni  7137  caucvgre  10985  xpscf  12760  bj-charfundcALT  14481