Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > neldifsn | Structured version Visualization version GIF version |
Description: The class 𝐴 is not in (𝐵 ∖ {𝐴}). (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
neldifsn | ⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neirr 2949 | . 2 ⊢ ¬ 𝐴 ≠ 𝐴 | |
2 | eldifsni 4703 | . 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐴}) → 𝐴 ≠ 𝐴) | |
3 | 1, 2 | mto 200 | 1 ⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2110 ≠ wne 2940 ∖ cdif 3863 {csn 4541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-v 3410 df-dif 3869 df-sn 4542 |
This theorem is referenced by: neldifsnd 4706 fofinf1o 8951 dfac9 9750 xrsupss 12899 hashgt23el 13991 fvsetsid 16721 islbs3 20192 islindf4 20800 ufinffr 22826 i1fd 24578 finsumvtxdg2sstep 27637 matunitlindflem1 35510 poimirlem25 35539 itg2addnclem 35565 itg2addnclem2 35566 prter2 36632 |
Copyright terms: Public domain | W3C validator |