Theorem ralbiia 2544

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

Syntax hints:   -> wi 4   <-> wb 105   e. wcel 2200   A.wral 2508

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 1493  ax-gen 1495

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

This theorem is referenced by:  frind  4447  poinxp  4793  soinxp  4794  seinxp  4795  dffun8  5352  funcnv3  5389  fncnv  5393  fnres  5446  fvreseq  5746  isoini2  5955  smores  6453  resixp  6897  pw1dc1  7099  finomni  7330  caucvgre  11532  xpscf  13420  mpodvdsmulf1o  15704  bj-charfundcALT  16340  cndcap  16599