Theorem ralimralim

Description: Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Assertion	ralimralim	|- ( A. x e. A ph -> A. x e. A ( ps -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		nfra1	|- F/ x A. x e. A ph
2		rspa	|- ( ( A. x e. A ph /\ x e. A ) -> ph )
3		ax-1	|- ( ph -> ( ps -> ph ) )
4	2 3	syl	|- ( ( A. x e. A ph /\ x e. A ) -> ( ps -> ph ) )
5	4	ex	|- ( A. x e. A ph -> ( x e. A -> ( ps -> ph ) ) )
6	1 5	ralrimi	|- ( A. x e. A ph -> A. x e. A ( ps -> ph ) )