Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > prnebg | Structured version Visualization version Unicode version |
Description: A (proper) pair is not equal to another (maybe improper) pair if and only if an element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 16-Jan-2018.) |
Ref | Expression |
---|---|
prnebg |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prneimg 4388 | . . 3 | |
2 | 1 | 3adant3 1081 | . 2 |
3 | ioran 511 | . . . . 5 | |
4 | ianor 509 | . . . . . . 7 | |
5 | nne 2798 | . . . . . . . 8 | |
6 | nne 2798 | . . . . . . . 8 | |
7 | 5, 6 | orbi12i 543 | . . . . . . 7 |
8 | 4, 7 | bitri 264 | . . . . . 6 |
9 | ianor 509 | . . . . . . 7 | |
10 | nne 2798 | . . . . . . . 8 | |
11 | nne 2798 | . . . . . . . 8 | |
12 | 10, 11 | orbi12i 543 | . . . . . . 7 |
13 | 9, 12 | bitri 264 | . . . . . 6 |
14 | 8, 13 | anbi12i 733 | . . . . 5 |
15 | 3, 14 | bitri 264 | . . . 4 |
16 | anddi 914 | . . . . 5 | |
17 | eqtr3 2643 | . . . . . . . . . 10 | |
18 | eqneqall 2805 | . . . . . . . . . 10 | |
19 | 17, 18 | syl 17 | . . . . . . . . 9 |
20 | preq12 4270 | . . . . . . . . . 10 | |
21 | 20 | a1d 25 | . . . . . . . . 9 |
22 | 19, 21 | jaoi 394 | . . . . . . . 8 |
23 | preq12 4270 | . . . . . . . . . . 11 | |
24 | prcom 4267 | . . . . . . . . . . 11 | |
25 | 23, 24 | syl6eq 2672 | . . . . . . . . . 10 |
26 | 25 | a1d 25 | . . . . . . . . 9 |
27 | eqtr3 2643 | . . . . . . . . . 10 | |
28 | 27, 18 | syl 17 | . . . . . . . . 9 |
29 | 26, 28 | jaoi 394 | . . . . . . . 8 |
30 | 22, 29 | jaoi 394 | . . . . . . 7 |
31 | 30 | com12 32 | . . . . . 6 |
32 | 31 | 3ad2ant3 1084 | . . . . 5 |
33 | 16, 32 | syl5bi 232 | . . . 4 |
34 | 15, 33 | syl5bi 232 | . . 3 |
35 | 34 | necon1ad 2811 | . 2 |
36 | 2, 35 | impbid 202 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 196 wo 383 wa 384 w3a 1037 wceq 1483 wcel 1990 wne 2794 cpr 4179 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-v 3202 df-un 3579 df-sn 4178 df-pr 4180 |
This theorem is referenced by: zlmodzxznm 42286 |
Copyright terms: Public domain | W3C validator |