![]() |
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 3788 | . . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V) | |
2 | falim 1550 | . . . 4 ⊢ (⊥ → 𝐴 ∈ V) | |
3 | 1, 2 | pm5.21ni 376 | . . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥)) |
4 | 3 | abbidv 2797 | . 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥}) |
5 | df-csb 3895 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
6 | fal 1547 | . . . 4 ⊢ ¬ ⊥ | |
7 | 6 | abf 4406 | . . 3 ⊢ {𝑦 ∣ ⊥} = ∅ |
8 | 7 | eqcomi 2737 | . 2 ⊢ ∅ = {𝑦 ∣ ⊥} |
9 | 4, 5, 8 | 3eqtr4g 2793 | 1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1533 ⊥wfal 1545 ∈ wcel 2098 {cab 2705 Vcvv 3473 [wsbc 3778 ⦋csb 3894 ∅c0 4326 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3475 df-sbc 3779 df-csb 3895 df-dif 3952 df-nul 4327 |
This theorem is referenced by: csb0 4411 sbcel12 4412 sbcne12 4416 sbcel2 4419 csbidm 4434 csbun 4442 csbin 4443 csbdif 4531 csbif 4589 csbuni 4943 sbcbr123 5206 sbcbr 5207 csbexg 5314 csbopab 5561 csbxp 5781 csbres 5992 csbima12 6087 csbrn 6212 csbiota 6546 csbfv12 6950 csbfv 6952 csbriota 7398 csbov123 7468 csbov 7469 |
Copyright terms: Public domain | W3C validator |