Theorem csb0

Description: The proper substitution of a class into the empty set is the empty set. (Contributed by NM, 18-Aug-2018)

	Ref	Expression
Assertion	csb0	⊢ ⦋ 𝐴 / 𝑥 ⦌ ∅ = ∅

Proof

Step	Hyp	Ref	Expression
1		csbconstg	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ∅ = ∅ )
2		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ∅ = ∅ )
3	1 2	pm2.61i	⊢ ⦋ 𝐴 / 𝑥 ⦌ ∅ = ∅