![]() |
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.) |
Ref | Expression |
---|---|
nelne2 | ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2893 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | |
2 | 1 | biimpcd 241 | . . 3 ⊢ (𝐴 ∈ 𝐶 → (𝐴 = 𝐵 → 𝐵 ∈ 𝐶)) |
3 | 2 | necon3bd 3012 | . 2 ⊢ (𝐴 ∈ 𝐶 → (¬ 𝐵 ∈ 𝐶 → 𝐴 ≠ 𝐵)) |
4 | 3 | imp 397 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 386 = wceq 1658 ∈ wcel 2166 ≠ wne 2998 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-ext 2802 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1881 df-cleq 2817 df-clel 2820 df-ne 2999 |
This theorem is referenced by: nelelne 3096 elnelne2 3112 elpwdifsn 4538 ac5num 9171 infpssrlem4 9442 fpwwe2lem13 9778 zgt1rpn0n1 12154 cats1un 13810 dprdfadd 18772 dprdcntz2 18790 lbsextlem4 19521 lindff1 20525 hauscmplem 21579 fileln0 22023 zcld 22985 dvcnvlem 24137 ppinprm 25290 chtnprm 25292 footex 26029 foot 26030 colperpexlem3 26040 mideulem2 26042 opphllem 26043 opphllem2 26056 lnopp2hpgb 26071 colhp 26078 lmieu 26092 trgcopy 26112 trgcopyeulem 26113 ordtconnlem1 30514 esum2dlem 30698 subfacp1lem5 31711 heiborlem6 34156 llnle 35592 lplnle 35614 lhpexle1lem 36081 cdleme18b 36366 cdlemg46 36809 cdlemh 36891 bcc0 39378 fnchoice 40005 climxrre 40776 stoweidlem43 41053 zneoALTV 42409 |
Copyright terms: Public domain | W3C validator |