Theorem csbexg

Description: The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005) (Revised by NM, 17-Aug-2018)

	Ref	Expression
Assertion	csbexg	⊢ ( ∀ 𝑥 𝐵 ∈ 𝑊 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 }
2		abid2	⊢ { 𝑦 ∣ 𝑦 ∈ 𝐵 } = 𝐵
3		elex	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
4	2 3	eqeltrid	⊢ ( 𝐵 ∈ 𝑊 → { 𝑦 ∣ 𝑦 ∈ 𝐵 } ∈ V )
5	4	alimi	⊢ ( ∀ 𝑥 𝐵 ∈ 𝑊 → ∀ 𝑥 { 𝑦 ∣ 𝑦 ∈ 𝐵 } ∈ V )
6		spsbc	⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 { 𝑦 ∣ 𝑦 ∈ 𝐵 } ∈ V → [ 𝐴 / 𝑥 ] { 𝑦 ∣ 𝑦 ∈ 𝐵 } ∈ V ) )
7	5 6	syl5	⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 𝐵 ∈ 𝑊 → [ 𝐴 / 𝑥 ] { 𝑦 ∣ 𝑦 ∈ 𝐵 } ∈ V ) )
8		nfcv	⊢ Ⅎ 𝑥 V
9	8	sbcabel	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] { 𝑦 ∣ 𝑦 ∈ 𝐵 } ∈ V ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } ∈ V ) )
10	7 9	sylibd	⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 𝐵 ∈ 𝑊 → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } ∈ V ) )
11	10	imp	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 𝐵 ∈ 𝑊 ) → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } ∈ V )
12	1 11	eqeltrid	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 𝐵 ∈ 𝑊 ) → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ V )
13		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∅ )
14		0ex	⊢ ∅ ∈ V
15	13 14	eqeltrdi	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ V )
16	15	adantr	⊢ ( ( ¬ 𝐴 ∈ V ∧ ∀ 𝑥 𝐵 ∈ 𝑊 ) → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ V )
17	12 16	pm2.61ian	⊢ ( ∀ 𝑥 𝐵 ∈ 𝑊 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ V )