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 2934 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵) | |
2 | 1 | neqned 3020 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∈ wcel 2105 ≠ wne 3013 |
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 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-clel 2890 df-ne 3014 |
This theorem is referenced by: nelelne 3114 elnelne2 3131 elneeldif 3947 elpwdifsn 4713 ac5num 9450 infpssrlem4 9716 fpwwe2lem13 10052 zgt1rpn0n1 12418 cats1un 14071 dprdfadd 19071 dprdcntz2 19089 lbsextlem4 19862 lindff1 20892 hauscmplem 21942 fileln0 22386 zcld 23348 dvcnvlem 24500 ppinprm 25656 chtnprm 25658 footexALT 26431 footexlem1 26432 footexlem2 26433 foot 26435 colperpexlem3 26445 mideulem2 26447 opphllem 26448 opphllem2 26461 lnopp2hpgb 26476 colhp 26483 lmieu 26497 trgcopy 26517 trgcopyeulem 26518 cycpmco2lem1 30695 cycpmco2 30702 cyc3genpmlem 30720 linds2eq 30868 lindsunlem 30919 fedgmul 30926 extdg1id 30952 ordtconnlem1 31066 esum2dlem 31250 subfacp1lem5 32328 heiborlem6 34975 llnle 36534 lplnle 36556 lhpexle1lem 37023 cdleme18b 37308 cdlemg46 37751 cdlemh 37833 bcc0 40549 fnchoice 41163 climxrre 41907 stoweidlem43 42205 zneoALTV 43711 |
Copyright terms: Public domain | W3C validator |