| 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 2865 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵) | |
| 2 | 1 | neqned 2947 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∈ wcel 2108 ≠ wne 2940 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-clel 2816 df-ne 2941 |
| This theorem is referenced by: nelelne 3041 elnelne2 3058 elneeldif 3965 elpwdifsn 4789 f1ounsn 7292 ac5num 10076 infpssrlem4 10346 fpwwe2lem12 10682 zgt1rpn0n1 13076 cats1un 14759 dprdfadd 20040 dprdcntz2 20058 lbsextlem4 21163 lindff1 21840 hauscmplem 23414 fileln0 23858 zcld 24835 dvcnvlem 26014 ppinprm 27195 chtnprm 27197 footexALT 28726 footexlem1 28727 footexlem2 28728 foot 28730 colperpexlem3 28740 mideulem2 28742 opphllem 28743 opphllem2 28756 lnopp2hpgb 28771 colhp 28778 lmieu 28792 trgcopy 28812 trgcopyeulem 28813 cycpmco2lem1 33146 cycpmco2 33153 cyc3genpmlem 33171 unitnz 33243 fracfld 33310 linds2eq 33409 elrspunsn 33457 mxidlnzr 33495 lindsunlem 33675 fedgmul 33682 extdg1id 33716 2sqr3minply 33791 ordtconnlem1 33923 esum2dlem 34093 subfacp1lem5 35189 heiborlem6 37823 llnle 39520 lplnle 39542 lhpexle1lem 40009 cdleme18b 40294 cdlemg46 40737 cdlemh 40819 ine1 42349 bcc0 44359 fnchoice 45034 climxrre 45765 stoweidlem43 46058 zneoALTV 47656 |
| Copyright terms: Public domain | W3C validator |