Theorem ra4

Description: Restricted quantifier version of Axiom 5 of Mendelson p. 69. This is the axiom stdpc5 of standard predicate calculus for a restricted domain. See ra4v for a version requiring fewer axioms. (Contributed by NM, 16-Jan-2004) (Proof shortened by BJ, 27-Mar-2020)

	Ref	Expression
Hypothesis	ra4.1	|- F/ x ph
Assertion	ra4	|- ( A. x e. A ( ph -> ps ) -> ( ph -> A. x e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		ra4.1	|- F/ x ph
2	1	r19.21	|- ( A. x e. A ( ph -> ps ) <-> ( ph -> A. x e. A ps ) )
3	2	biimpi	|- ( A. x e. A ( ph -> ps ) -> ( ph -> A. x e. A ps ) )