![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nbrne2 | Structured version Visualization version Unicode 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 4418 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpcd 232 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | necon3bd 2649 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | imp 435 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-rab 2757 df-v 3058 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-br 4416 |
This theorem is referenced by: frfi 7841 hl2at 33014 2atjm 33054 atbtwn 33055 atbtwnexOLDN 33056 atbtwnex 33057 dalem21 33303 dalem23 33305 dalem27 33308 dalem54 33335 2llnma1b 33395 lhpexle1lem 33616 lhpexle3lem 33620 lhp2at0nle 33644 4atexlemunv 33675 4atexlemnclw 33679 4atexlemcnd 33681 cdlemc5 33805 cdleme0b 33822 cdleme0c 33823 cdleme0fN 33828 cdleme01N 33831 cdleme0ex2N 33834 cdleme3b 33839 cdleme3c 33840 cdleme3g 33844 cdleme3h 33845 cdleme7aa 33852 cdleme7b 33854 cdleme7c 33855 cdleme7d 33856 cdleme7e 33857 cdleme7ga 33858 cdleme11fN 33874 cdlemesner 33906 cdlemednpq 33909 cdleme19a 33914 cdleme19c 33916 cdleme21c 33938 cdleme21ct 33940 cdleme22cN 33953 cdleme22f2 33958 cdleme22g 33959 cdleme41sn3aw 34085 cdlemeg46rgv 34139 cdlemeg46req 34140 cdlemf1 34172 cdlemg27b 34307 cdlemg33b0 34312 cdlemg33c0 34313 cdlemh 34428 cdlemk14 34465 dia2dimlem1 34676 |
Copyright terms: Public domain | W3C validator |