Theorem ralbiia 2508

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 2504	1 |- ( A. x e. A ph <-> A. x e. A ps )

Syntax hints:   -> wi 4   <-> wb 105   e. wcel 2164   A.wral 2472

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 1458  ax-gen 1460

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

This theorem is referenced by:  frind  4384  poinxp  4729  soinxp  4730  seinxp  4731  dffun8  5283  funcnv3  5317  fncnv  5321  fnres  5371  fvreseq  5662  isoini2  5863  smores  6347  resixp  6789  pw1dc1  6972  finomni  7201  caucvgre  11128  xpscf  12933  bj-charfundcALT  15371  cndcap  15619