![]() |
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 2853 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵) | |
2 | 1 | neqned 2944 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 394 ∈ wcel 2098 ≠ wne 2937 |
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-ex 1774 df-cleq 2720 df-clel 2806 df-ne 2938 |
This theorem is referenced by: nelelne 3038 elnelne2 3055 elneeldif 3963 elpwdifsn 4797 ac5num 10067 infpssrlem4 10337 fpwwe2lem12 10673 zgt1rpn0n1 13055 cats1un 14711 dprdfadd 19984 dprdcntz2 20002 lbsextlem4 21056 lindff1 21761 hauscmplem 23330 fileln0 23774 zcld 24749 dvcnvlem 25928 ppinprm 27104 chtnprm 27106 footexALT 28542 footexlem1 28543 footexlem2 28544 foot 28546 colperpexlem3 28556 mideulem2 28558 opphllem 28559 opphllem2 28572 lnopp2hpgb 28587 colhp 28594 lmieu 28608 trgcopy 28628 trgcopyeulem 28629 cycpmco2lem1 32868 cycpmco2 32875 cyc3genpmlem 32893 unitnz 32967 fracfld 33019 linds2eq 33121 elrspunsn 33170 mxidlnzr 33205 lindsunlem 33355 fedgmul 33362 extdg1id 33388 ordtconnlem1 33558 esum2dlem 33744 subfacp1lem5 34827 heiborlem6 37322 llnle 39023 lplnle 39045 lhpexle1lem 39512 cdleme18b 39797 cdlemg46 40240 cdlemh 40322 ine1 41906 bcc0 43808 fnchoice 44422 climxrre 45167 stoweidlem43 45460 zneoALTV 47038 |
Copyright terms: Public domain | W3C validator |