Theorem alrimii

Description: A lemma for introducing a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019)

	Ref	Expression
Hypotheses	alrimii.1	|- F/ y ph
	alrimii.2	|- ( ph -> ps )
	alrimii.3	|- ( [. y / x ]. ch <-> ps )
	alrimii.4	|- F/ y ch
Assertion	alrimii	|- ( ph -> A. x ch )

Proof

Step	Hyp	Ref	Expression
1		alrimii.1	|- F/ y ph
2		alrimii.2	|- ( ph -> ps )
3		alrimii.3	|- ( [. y / x ]. ch <-> ps )
4		alrimii.4	|- F/ y ch
5	2 3	sylibr	|- ( ph -> [. y / x ]. ch )
6	1 5	alrimi	|- ( ph -> A. y [. y / x ]. ch )
7		nfsbc1v	|- F/ x [. y / x ]. ch
8		sbceq2a	|- ( y = x -> ( [. y / x ]. ch <-> ch ) )
9	7 4 8	cbvalv1	|- ( A. y [. y / x ]. ch <-> A. x ch )
10	6 9	sylib	|- ( ph -> A. x ch )