![]() |
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 3711 | . . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V) | |
2 | falim 1537 | . . . 4 ⊢ (⊥ → 𝐴 ∈ V) | |
3 | 1, 2 | pm5.21ni 379 | . . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥)) |
4 | 3 | abbidv 2858 | . 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥}) |
5 | df-csb 3807 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
6 | fal 1534 | . . . 4 ⊢ ¬ ⊥ | |
7 | 6 | abf 4270 | . . 3 ⊢ {𝑦 ∣ ⊥} = ∅ |
8 | 7 | eqcomi 2802 | . 2 ⊢ ∅ = {𝑦 ∣ ⊥} |
9 | 4, 5, 8 | 3eqtr4g 2854 | 1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1520 ⊥wfal 1532 ∈ wcel 2079 {cab 2773 Vcvv 3432 [wsbc 3701 ⦋csb 3806 ∅c0 4206 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-ext 2767 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1523 df-fal 1533 df-ex 1760 df-nf 1764 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-nul 4207 |
This theorem is referenced by: csb0 4273 sbcel12 4274 sbcne12 4278 sbcel2 4281 csbidm 4291 csbun 4299 csbin 4300 csbif 4430 csbuni 4767 sbcbr123 5010 sbcbr 5011 csbexg 5099 csbopab 5322 csbxp 5528 csbres 5729 csbima12 5815 csbrn 5927 csbiota 6210 csbfv12 6573 csbfv 6575 csbriota 6980 csbov123 7048 csbov 7049 csbdif 34083 |
Copyright terms: Public domain | W3C validator |