Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > csbprc | Structured version Visualization version GIF version |
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 |
---|---|
csbprc | ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcex 3779 | . . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V) | |
2 | falim 1545 | . . . 4 ⊢ (⊥ → 𝐴 ∈ V) | |
3 | 1, 2 | pm5.21ni 379 | . . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥)) |
4 | 3 | abbidv 2882 | . 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥}) |
5 | df-csb 3881 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
6 | fal 1542 | . . . 4 ⊢ ¬ ⊥ | |
7 | 6 | abf 4353 | . . 3 ⊢ {𝑦 ∣ ⊥} = ∅ |
8 | 7 | eqcomi 2827 | . 2 ⊢ ∅ = {𝑦 ∣ ⊥} |
9 | 4, 5, 8 | 3eqtr4g 2878 | 1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ⊥wfal 1540 ∈ wcel 2105 {cab 2796 Vcvv 3492 [wsbc 3769 ⦋csb 3880 ∅c0 4288 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-fal 1541 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-sbc 3770 df-csb 3881 df-dif 3936 df-nul 4289 |
This theorem is referenced by: csb0 4356 sbcel12 4357 sbcne12 4361 sbcel2 4364 csbidm 4379 csbun 4387 csbin 4388 csbif 4518 csbuni 4858 sbcbr123 5111 sbcbr 5112 csbexg 5205 csbopab 5433 csbxp 5643 csbres 5849 csbima12 5940 csbrn 6053 csbiota 6341 csbfv12 6706 csbfv 6708 csbriota 7118 csbov123 7187 csbov 7188 csbdif 34488 |
Copyright terms: Public domain | W3C validator |