![]() |
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 3586 | . . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V) | |
2 | falim 1647 | . . . 4 ⊢ (⊥ → 𝐴 ∈ V) | |
3 | 1, 2 | pm5.21ni 366 | . . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥)) |
4 | 3 | abbidv 2879 | . 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥}) |
5 | df-csb 3675 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
6 | fal 1639 | . . . 4 ⊢ ¬ ⊥ | |
7 | 6 | abf 4121 | . . 3 ⊢ {𝑦 ∣ ⊥} = ∅ |
8 | 7 | eqcomi 2769 | . 2 ⊢ ∅ = {𝑦 ∣ ⊥} |
9 | 4, 5, 8 | 3eqtr4g 2819 | 1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1632 ⊥wfal 1637 ∈ wcel 2139 {cab 2746 Vcvv 3340 [wsbc 3576 ⦋csb 3674 ∅c0 4058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-fal 1638 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-v 3342 df-sbc 3577 df-csb 3675 df-dif 3718 df-nul 4059 |
This theorem is referenced by: csb0 4125 sbcel12 4126 sbcne12 4129 sbcel2 4132 csbidm 4145 csbun 4152 csbin 4153 csbif 4282 csbuni 4618 sbcbr123 4858 sbcbr 4859 csbexg 4944 csbopab 5158 csbxp 5357 csbres 5554 csbima12 5641 csbrn 5754 csbiota 6042 csbfv12 6392 csbfv 6394 csbriota 6786 csbov123 6850 csbov 6851 csbdif 33482 |
Copyright terms: Public domain | W3C validator |