This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )