Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nbrne2 | Structured version Visualization version GIF version |
Description: Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.) |
Ref | Expression |
---|---|
nbrne2 | ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1 4586 | . . . 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 ≠ wne 2780 class class class wbr 4583 |
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-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 |
This theorem is referenced by: frfi 8090 hl2at 33709 2atjm 33749 atbtwn 33750 atbtwnexOLDN 33751 atbtwnex 33752 dalem21 33998 dalem23 34000 dalem27 34003 dalem54 34030 2llnma1b 34090 lhpexle1lem 34311 lhpexle3lem 34315 lhp2at0nle 34339 4atexlemunv 34370 4atexlemnclw 34374 4atexlemcnd 34376 cdlemc5 34500 cdleme0b 34517 cdleme0c 34518 cdleme0fN 34523 cdleme01N 34526 cdleme0ex2N 34529 cdleme3b 34534 cdleme3c 34535 cdleme3g 34539 cdleme3h 34540 cdleme7aa 34547 cdleme7b 34549 cdleme7c 34550 cdleme7d 34551 cdleme7e 34552 cdleme7ga 34553 cdleme11fN 34569 cdlemesner 34601 cdlemednpq 34604 cdleme19a 34609 cdleme19c 34611 cdleme21c 34633 cdleme21ct 34635 cdleme22cN 34648 cdleme22f2 34653 cdleme22g 34654 cdleme41sn3aw 34780 cdlemeg46rgv 34834 cdlemeg46req 34835 cdlemf1 34867 cdlemg27b 35002 cdlemg33b0 35007 cdlemg33c0 35008 cdlemh 35123 cdlemk14 35160 dia2dimlem1 35371 |
Copyright terms: Public domain | W3C validator |