Theorem ralbiia 2520

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

Syntax hints:   -> wi 4   <-> wb 105   e. wcel 2176   A.wral 2484

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 1470  ax-gen 1472

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

This theorem is referenced by:  frind  4400  poinxp  4745  soinxp  4746  seinxp  4747  dffun8  5300  funcnv3  5337  fncnv  5341  fnres  5394  fvreseq  5685  isoini2  5890  smores  6380  resixp  6822  pw1dc1  7013  finomni  7244  caucvgre  11325  xpscf  13212  mpodvdsmulf1o  15495  bj-charfundcALT  15782  cndcap  16035