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 2863 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵) | |
2 | 1 | neqned 2950 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∈ wcel 2106 ≠ wne 2943 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-cleq 2730 df-clel 2816 df-ne 2944 |
This theorem is referenced by: nelelne 3043 elnelne2 3060 elneeldif 3901 elpwdifsn 4722 ac5num 9792 infpssrlem4 10062 fpwwe2lem12 10398 zgt1rpn0n1 12771 cats1un 14434 dprdfadd 19623 dprdcntz2 19641 lbsextlem4 20423 lindff1 21027 hauscmplem 22557 fileln0 23001 zcld 23976 dvcnvlem 25140 ppinprm 26301 chtnprm 26303 footexALT 27079 footexlem1 27080 footexlem2 27081 foot 27083 colperpexlem3 27093 mideulem2 27095 opphllem 27096 opphllem2 27109 lnopp2hpgb 27124 colhp 27131 lmieu 27145 trgcopy 27165 trgcopyeulem 27166 cycpmco2lem1 31393 cycpmco2 31400 cyc3genpmlem 31418 linds2eq 31575 mxidlnzr 31639 lindsunlem 31705 fedgmul 31712 extdg1id 31738 ordtconnlem1 31874 esum2dlem 32060 subfacp1lem5 33146 heiborlem6 35974 llnle 37532 lplnle 37554 lhpexle1lem 38021 cdleme18b 38306 cdlemg46 38749 cdlemh 38831 bcc0 41958 fnchoice 42572 climxrre 43291 stoweidlem43 43584 zneoALTV 45121 |
Copyright terms: Public domain | W3C validator |