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	$$⊢Ⅎy\phi$$
	alrimii.2	$$⊢\phi \to \psi$$
	alrimii.3	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\chi \leftrightarrow \psi$$
	alrimii.4	$$⊢Ⅎy\chi$$
Assertion	alrimii	$$⊢\phi \to \forall x\chi$$

Proof

Step	Hyp	Ref	Expression
1		alrimii.1	$$⊢Ⅎy\phi$$
2		alrimii.2	$$⊢\phi \to \psi$$
3		alrimii.3	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\chi \leftrightarrow \psi$$
4		alrimii.4	$$⊢Ⅎy\chi$$
5	2 3	sylibr	$$⊢\phi \to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\chi$$
6	1 5	alrimi	$$⊢\phi \to \forall y\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\chi$$
7		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\chi$$
8		sbceq2a	$$⊢y=x\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\chi \leftrightarrow \chi \right)$$
9	7 4 8	cbvalv1	$$⊢\forall y\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\chi \leftrightarrow \forall x\chi$$
10	6 9	sylib	$$⊢\phi \to \forall x\chi$$