Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nelne2 | Structured version Visualization version GIF version |
Description: Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.) (Proof shortened by Wolf Lammen, 14-May-2023.) |
Ref | Expression |
---|---|
nelne2 | ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nelneq 2857 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵) | |
2 | 1 | neqned 2941 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 ∈ wcel 2113 ≠ wne 2934 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-cleq 2730 df-clel 2811 df-ne 2935 |
This theorem is referenced by: nelelne 3032 elnelne2 3049 elneeldif 3855 elpwdifsn 4674 ac5num 9529 infpssrlem4 9799 fpwwe2lem12 10135 zgt1rpn0n1 12506 cats1un 14165 dprdfadd 19254 dprdcntz2 19272 lbsextlem4 20045 lindff1 20629 hauscmplem 22150 fileln0 22594 zcld 23558 dvcnvlem 24720 ppinprm 25881 chtnprm 25883 footexALT 26656 footexlem1 26657 footexlem2 26658 foot 26660 colperpexlem3 26670 mideulem2 26672 opphllem 26673 opphllem2 26686 lnopp2hpgb 26701 colhp 26708 lmieu 26722 trgcopy 26742 trgcopyeulem 26743 cycpmco2lem1 30962 cycpmco2 30969 cyc3genpmlem 30987 linds2eq 31139 mxidlnzr 31203 lindsunlem 31269 fedgmul 31276 extdg1id 31302 ordtconnlem1 31438 esum2dlem 31622 subfacp1lem5 32709 heiborlem6 35586 llnle 37144 lplnle 37166 lhpexle1lem 37633 cdleme18b 37918 cdlemg46 38361 cdlemh 38443 bcc0 41480 fnchoice 42094 climxrre 42817 stoweidlem43 43110 zneoALTV 44639 |
Copyright terms: Public domain | W3C validator |