Theorem sbali

Description: Discard class substitution in a universal quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019)

	Ref	Expression
Hypothesis	sbali.1	⊢ 𝐴 ∈ V
Assertion	sbali	⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbali.1	⊢ 𝐴 ∈ V
2		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 𝜑
3	1 2	sbcgfi	⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜑 )