Description: There is (at least) one set with two different elements: the unordered pair containing 0 and 1 . In contrast to pr0hash2ex , numbers are used instead of sets because their representation is shorter (and more comprehensive). (Contributed by AV, 29-Jan-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | prhash2ex | |- ( # ` { 0 , 1 } ) = 2 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0ne1 | |- 0 =/= 1 |
|
| 2 | c0ex | |- 0 e. _V |
|
| 3 | 1ex | |- 1 e. _V |
|
| 4 | hashprg | |- ( ( 0 e. _V /\ 1 e. _V ) -> ( 0 =/= 1 <-> ( # ` { 0 , 1 } ) = 2 ) ) |
|
| 5 | 4 | bicomd | |- ( ( 0 e. _V /\ 1 e. _V ) -> ( ( # ` { 0 , 1 } ) = 2 <-> 0 =/= 1 ) ) |
| 6 | 2 3 5 | mp2an | |- ( ( # ` { 0 , 1 } ) = 2 <-> 0 =/= 1 ) |
| 7 | 1 6 | mpbir | |- ( # ` { 0 , 1 } ) = 2 |