![]() |
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 2858 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵) | |
2 | 1 | neqned 2947 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 ∈ wcel 2107 ≠ wne 2940 |
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-ex 1783 df-cleq 2725 df-clel 2811 df-ne 2941 |
This theorem is referenced by: nelelne 3040 elnelne2 3057 elneeldif 3925 elpwdifsn 4750 ac5num 9977 infpssrlem4 10247 fpwwe2lem12 10583 zgt1rpn0n1 12961 cats1un 14615 dprdfadd 19804 dprdcntz2 19822 lbsextlem4 20638 lindff1 21242 hauscmplem 22773 fileln0 23217 zcld 24192 dvcnvlem 25356 ppinprm 26517 chtnprm 26519 footexALT 27702 footexlem1 27703 footexlem2 27704 foot 27706 colperpexlem3 27716 mideulem2 27718 opphllem 27719 opphllem2 27732 lnopp2hpgb 27747 colhp 27754 lmieu 27768 trgcopy 27788 trgcopyeulem 27789 cycpmco2lem1 32024 cycpmco2 32031 cyc3genpmlem 32049 linds2eq 32216 mxidlnzr 32284 lindsunlem 32376 fedgmul 32383 extdg1id 32409 ordtconnlem1 32562 esum2dlem 32748 subfacp1lem5 33835 heiborlem6 36321 llnle 38027 lplnle 38049 lhpexle1lem 38516 cdleme18b 38801 cdlemg46 39244 cdlemh 39326 bcc0 42708 fnchoice 43322 climxrre 44077 stoweidlem43 44370 zneoALTV 45947 |
Copyright terms: Public domain | W3C validator |