Theorem csbprc

Description: The proper substitution of a proper class for a set into a class results in the empty set. (Contributed by NM, 17-Aug-2018) (Proof shortened by JJ, 27-Aug-2021)

	Ref	Expression
Assertion	csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		sbcex	⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 → 𝐴 ∈ V )
2		falim	⊢ ( ⊥ → 𝐴 ∈ V )
3	1 2	pm5.21ni	⊢ ( ¬ 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ ⊥ ) )
4	3	abbidv	⊢ ( ¬ 𝐴 ∈ V → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ ⊥ } )
5		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 }
6		fal	⊢ ¬ ⊥
7	6	abf	⊢ { 𝑦 ∣ ⊥ } = ∅
8	7	eqcomi	⊢ ∅ = { 𝑦 ∣ ⊥ }
9	4 5 8	3eqtr4g	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∅ )