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 2676 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | |
2 | 1 | biimpcd 238 | . . 3 ⊢ (𝐴 ∈ 𝐶 → (𝐴 = 𝐵 → 𝐵 ∈ 𝐶)) |
3 | 2 | necon3bd 2796 | . 2 ⊢ (𝐴 ∈ 𝐶 → (¬ 𝐵 ∈ 𝐶 → 𝐴 ≠ 𝐵)) |
4 | 3 | imp 444 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-cleq 2603 df-clel 2606 df-ne 2782 |
This theorem is referenced by: nelelne 2880 elnelne2 2894 ac5num 8742 infpssrlem4 9011 fpwwe2lem13 9343 zgt1rpn0n1 11747 cats1un 13327 dprdfadd 18242 dprdcntz2 18260 lbsextlem4 18982 lindff1 19978 hauscmplem 21019 fileln0 21464 zcld 22424 dvcnvlem 23543 ppinprm 24678 chtnprm 24680 footex 25413 foot 25414 colperpexlem3 25424 mideulem2 25426 opphllem 25427 opphllem2 25440 lnopp2hpgb 25455 colhp 25462 lmieu 25476 trgcopy 25496 trgcopyeulem 25497 eupap1 26503 ordtconlem1 29298 esum2dlem 29481 subfacp1lem5 30420 heiborlem6 32785 llnle 33822 lplnle 33844 lhpexle1lem 34311 cdleme18b 34597 cdlemg46 35041 cdlemh 35123 bcc0 37561 fnchoice 38211 stoweidlem43 38936 zneoALTV 40118 elpwdifsn 40312 |
Copyright terms: Public domain | W3C validator |