![]() |
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 3750 | . . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V) | |
2 | falim 1559 | . . . 4 ⊢ (⊥ → 𝐴 ∈ V) | |
3 | 1, 2 | pm5.21ni 379 | . . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥)) |
4 | 3 | abbidv 2802 | . 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥}) |
5 | df-csb 3857 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
6 | fal 1556 | . . . 4 ⊢ ¬ ⊥ | |
7 | 6 | abf 4363 | . . 3 ⊢ {𝑦 ∣ ⊥} = ∅ |
8 | 7 | eqcomi 2742 | . 2 ⊢ ∅ = {𝑦 ∣ ⊥} |
9 | 4, 5, 8 | 3eqtr4g 2798 | 1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ⊥wfal 1554 ∈ wcel 2107 {cab 2710 Vcvv 3444 [wsbc 3740 ⦋csb 3856 ∅c0 4283 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3446 df-sbc 3741 df-csb 3857 df-dif 3914 df-nul 4284 |
This theorem is referenced by: csb0 4368 sbcel12 4369 sbcne12 4373 sbcel2 4376 csbidm 4391 csbun 4399 csbin 4400 csbdif 4486 csbif 4544 csbuni 4898 sbcbr123 5160 sbcbr 5161 csbexg 5268 csbopab 5513 csbxp 5732 csbres 5941 csbima12 6032 csbrn 6156 csbiota 6490 csbfv12 6891 csbfv 6893 csbriota 7330 csbov123 7400 csbov 7401 |
Copyright terms: Public domain | W3C validator |