Metamath Proof Explorer

Theorem csb0

Description: The proper substitution of a class into the empty set is the empty set. (Contributed by NM, 18-Aug-2018) Avoid ax-12 . (Revised by Gino Giotto, 28-Jun-2024)

Ref Expression
Assertion csb0 ⊢ ⦋ A / x⦌ ∅ = ∅

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ _ x ∅
2 df-csb ⊢ ⦋ A / x⦌ ∅ = y | [˙A / x]˙ y ∈ ∅
3 dfsbcq2 ⊢ z = A → z x y ∈ ∅ ↔ [˙A / x]˙ y ∈ ∅
4 3 bibi1d ⊢ z = A → z x y ∈ ∅ ↔ y ∈ ∅ ↔ [˙A / x]˙ y ∈ ∅ ↔ y ∈ ∅
5 4 imbi2d ⊢ z = A → Ⅎ x y ∈ ∅ → z x y ∈ ∅ ↔ y ∈ ∅ ↔ Ⅎ x y ∈ ∅ → [˙A / x]˙ y ∈ ∅ ↔ y ∈ ∅
6 sbv ⊢ z x y ∈ ∅ ↔ y ∈ ∅
7 6 a1i ⊢ Ⅎ x y ∈ ∅ → z x y ∈ ∅ ↔ y ∈ ∅
8 5 7 vtoclg ⊢ A ∈ V → Ⅎ x y ∈ ∅ → [˙A / x]˙ y ∈ ∅ ↔ y ∈ ∅
9 nfcr ⊢ Ⅎ _ x ∅ → Ⅎ x y ∈ ∅
10 8 9 impel ⊢ A ∈ V ∧ Ⅎ _ x ∅ → [˙A / x]˙ y ∈ ∅ ↔ y ∈ ∅
11 10 abbi1dv ⊢ A ∈ V ∧ Ⅎ _ x ∅ → y | [˙A / x]˙ y ∈ ∅ = ∅
12 2 11 syl5eq ⊢ A ∈ V ∧ Ⅎ _ x ∅ → ⦋ A / x⦌ ∅ = ∅
13 1 12 mpan2 ⊢ A ∈ V → ⦋ A / x⦌ ∅ = ∅
14 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ ∅ = ∅
15 13 14 pm2.61i ⊢ ⦋ A / x⦌ ∅ = ∅