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 2937 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵) | |
2 | 1 | neqned 3023 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∈ wcel 2105 ≠ wne 3016 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-clel 2893 df-ne 3017 |
This theorem is referenced by: nelelne 3117 elnelne2 3134 elneeldif 3949 elpwdifsn 4715 ac5num 9451 infpssrlem4 9717 fpwwe2lem13 10053 zgt1rpn0n1 12420 cats1un 14073 dprdfadd 19073 dprdcntz2 19091 lbsextlem4 19864 lindff1 20894 hauscmplem 21944 fileln0 22388 zcld 23350 dvcnvlem 24502 ppinprm 25657 chtnprm 25659 footexALT 26432 footexlem1 26433 footexlem2 26434 foot 26436 colperpexlem3 26446 mideulem2 26448 opphllem 26449 opphllem2 26462 lnopp2hpgb 26477 colhp 26484 lmieu 26498 trgcopy 26518 trgcopyeulem 26519 cycpmco2lem1 30696 cycpmco2 30703 cyc3genpmlem 30721 linds2eq 30869 lindsunlem 30920 fedgmul 30927 extdg1id 30953 ordtconnlem1 31067 esum2dlem 31251 subfacp1lem5 32329 heiborlem6 34977 llnle 36536 lplnle 36558 lhpexle1lem 37025 cdleme18b 37310 cdlemg46 37753 cdlemh 37835 bcc0 40552 fnchoice 41166 climxrre 41911 stoweidlem43 42209 zneoALTV 43681 |
Copyright terms: Public domain | W3C validator |