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 5060 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | |
2 | 1 | biimpcd 250 | . . 3 ⊢ (𝐴𝑅𝐶 → (𝐴 = 𝐵 → 𝐵𝑅𝐶)) |
3 | 2 | necon3bd 3027 | . 2 ⊢ (𝐴𝑅𝐶 → (¬ 𝐵𝑅𝐶 → 𝐴 ≠ 𝐵)) |
4 | 3 | imp 407 | 1 ⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1528 ≠ wne 3013 class class class wbr 5057 |
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-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 |
This theorem is referenced by: frfi 8751 ablsimpgfindlem1 19158 ablsimpgfindlem2 19159 hl2at 36421 2atjm 36461 atbtwn 36462 atbtwnexOLDN 36463 atbtwnex 36464 dalem21 36710 dalem23 36712 dalem27 36715 dalem54 36742 2llnma1b 36802 lhpexle1lem 37023 lhpexle3lem 37027 lhp2at0nle 37051 4atexlemunv 37082 4atexlemnclw 37086 4atexlemcnd 37088 cdlemc5 37211 cdleme0b 37228 cdleme0c 37229 cdleme0fN 37234 cdleme01N 37237 cdleme0ex2N 37240 cdleme3b 37245 cdleme3c 37246 cdleme3g 37250 cdleme3h 37251 cdleme7aa 37258 cdleme7b 37260 cdleme7c 37261 cdleme7d 37262 cdleme7e 37263 cdleme7ga 37264 cdleme11fN 37280 cdlemesner 37312 cdlemednpq 37315 cdleme19a 37319 cdleme19c 37321 cdleme21c 37343 cdleme21ct 37345 cdleme22cN 37358 cdleme22f2 37363 cdleme22g 37364 cdleme41sn3aw 37490 cdlemeg46rgv 37544 cdlemeg46req 37545 cdlemf1 37577 cdlemg27b 37712 cdlemg33b0 37717 cdlemg33c0 37718 cdlemh 37833 cdlemk14 37870 dia2dimlem1 38080 |
Copyright terms: Public domain | W3C validator |