Theorem ralbiia 2564

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  frind  4499  poinxp  4846  soinxp  4847  seinxp  4848  dffun8  5408  funcnv3  5446  fncnv  5450  fnres  5503  fvreseq  5815  isoini2  6028  smores  6567  resixp  7019  pw1dc1  7225  finomni  7486  caucvgre  11769  xpscf  13727  mpodvdsmulf1o  16284  bj-charfundcALT  17040  cndcap  17316