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  4353  poinxp  4696  soinxp  4697  seinxp  4698  dffun8  5245  funcnv3  5279  fncnv  5283  fnres  5333  fvreseq  5620  isoini2  5820  smores  6293  resixp  6733  pw1dc1  6913  finomni  7138  caucvgre  10990  xpscf  12766  bj-charfundcALT  14564