Theorem bj-csbprc

Description: More direct proof of csbprc (fewer essential steps). (Contributed by BJ, 24-Jul-2019) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 }
2		sbcex	⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 → 𝐴 ∈ V )
3	2	con3i	⊢ ( ¬ 𝐴 ∈ V → ¬ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 )
4	3	alrimiv	⊢ ( ¬ 𝐴 ∈ V → ∀ 𝑦 ¬ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 )
5		bj-ab0	⊢ ( ∀ 𝑦 ¬ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = ∅ )
6	4 5	syl	⊢ ( ¬ 𝐴 ∈ V → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = ∅ )
7	1 6	eqtrid	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∅ )