Theorem sbexi

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

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

Proof

Step	Hyp	Ref	Expression
1		sbexi.1	⊢ 𝐴 ∈ V
2		nfe1	⊢ Ⅎ 𝑥 ∃ 𝑥 𝜑
3	1 2	sbcgfi	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑥 𝜑 ↔ ∃ 𝑥 𝜑 )