Theorem r19.21

Description: Restricted quantifier version of 19.21 . (Contributed by Scott Fenton, 30-Mar-2011)

	Ref	Expression
Hypothesis	r19.21.1	|- F/ x ph
Assertion	r19.21	|- ( A. x e. A ( ph -> ps ) <-> ( ph -> A. x e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		r19.21.1	|- F/ x ph
2		r19.21t	|- ( F/ x ph -> ( A. x e. A ( ph -> ps ) <-> ( ph -> A. x e. A ps ) ) )
3	1 2	ax-mp	|- ( A. x e. A ( ph -> ps ) <-> ( ph -> A. x e. A ps ) )