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	⊢ Ⅎ 𝑦 𝜑
	alrimii.2	⊢ ( 𝜑 → 𝜓 )
	alrimii.3	⊢ ( [ 𝑦 / 𝑥 ] 𝜒 ↔ 𝜓 )
	alrimii.4	⊢ Ⅎ 𝑦 𝜒
Assertion	alrimii	⊢ ( 𝜑 → ∀ 𝑥 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		alrimii.1	⊢ Ⅎ 𝑦 𝜑
2		alrimii.2	⊢ ( 𝜑 → 𝜓 )
3		alrimii.3	⊢ ( [ 𝑦 / 𝑥 ] 𝜒 ↔ 𝜓 )
4		alrimii.4	⊢ Ⅎ 𝑦 𝜒
5	2 3	sylibr	⊢ ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜒 )
6	1 5	alrimi	⊢ ( 𝜑 → ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜒 )
7		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜒
8		sbceq2a	⊢ ( 𝑦 = 𝑥 → ( [ 𝑦 / 𝑥 ] 𝜒 ↔ 𝜒 ) )
9	7 4 8	cbvalv1	⊢ ( ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜒 ↔ ∀ 𝑥 𝜒 )
10	6 9	sylib	⊢ ( 𝜑 → ∀ 𝑥 𝜒 )