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 ⊢ ∀ x B ∈ W → ⦋ A / x⦌ B ∈ V

Proof

Step Hyp Ref Expression
1 df-csb ⊢ ⦋ A / x⦌ B = y | [˙A / x]˙ y ∈ B
2 abid2 ⊢ y | y ∈ B = B
3 elex ⊢ B ∈ W → B ∈ V
4 2 3 eqeltrid ⊢ B ∈ W → y | y ∈ B ∈ V
5 4 alimi ⊢ ∀ x B ∈ W → ∀ x y | y ∈ B ∈ V
6 spsbc ⊢ A ∈ V → ∀ x y | y ∈ B ∈ V → [˙A / x]˙ y | y ∈ B ∈ V
7 5 6 syl5 ⊢ A ∈ V → ∀ x B ∈ W → [˙A / x]˙ y | y ∈ B ∈ V
8 nfcv ⊢ Ⅎ _ x V
9 8 sbcabel ⊢ A ∈ V → [˙A / x]˙ y | y ∈ B ∈ V ↔ y | [˙A / x]˙ y ∈ B ∈ V
10 7 9 sylibd ⊢ A ∈ V → ∀ x B ∈ W → y | [˙A / x]˙ y ∈ B ∈ V
11 10 imp ⊢ A ∈ V ∧ ∀ x B ∈ W → y | [˙A / x]˙ y ∈ B ∈ V
12 1 11 eqeltrid ⊢ A ∈ V ∧ ∀ x B ∈ W → ⦋ A / x⦌ B ∈ V
13 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ B = ∅
14 0ex ⊢ ∅ ∈ V
15 13 14 eqeltrdi ⊢ ¬ A ∈ V → ⦋ A / x⦌ B ∈ V
16 15 adantr ⊢ ¬ A ∈ V ∧ ∀ x B ∈ W → ⦋ A / x⦌ B ∈ V
17 12 16 pm2.61ian ⊢ ∀ x B ∈ W → ⦋ A / x⦌ B ∈ V