Description: The proper substitution of a proper class for a set into a class results in the empty set. (Contributed by NM, 17-Aug-2018) (Proof shortened by JJ, 27-Aug-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | csbprc | ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∅ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbcex | ⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 → 𝐴 ∈ V ) | |
| 2 | falim | ⊢ ( ⊥ → 𝐴 ∈ V ) | |
| 3 | 1 2 | pm5.21ni | ⊢ ( ¬ 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ ⊥ ) ) |
| 4 | 3 | abbidv | ⊢ ( ¬ 𝐴 ∈ V → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ ⊥ } ) |
| 5 | df-csb | ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } | |
| 6 | dfnul4 | ⊢ ∅ = { 𝑦 ∣ ⊥ } | |
| 7 | 4 5 6 | 3eqtr4g | ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∅ ) |