| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Strict dominance implies non-equinumerosity. |
| Ref | Expression |
|---|---|
| sdomnen |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brsdom 4520 |
. 2
| |
| 2 | 1 | pm3.27bi 324 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: bren2 4528 sdomnsym 4605 domnsym 4606 sdomdomtr 4612 sdomirr 4615 php5 4662 pssinf 4672 isfinite2 4690 pm54.43 4713 cardnn 4968 cardom 4970 ondomcard 5005 top2ind 11014 omsubsdom 11402 omsubdom 11403 omsubel 11404 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 997 ax-gen 998 ax-8 999 ax-10 1001 ax-12 1003 ax-17 1006 ax-4 1008 ax-5o 1010 ax-6o 1013 ax-9o 1158 ax-10o 1176 ax-16 1246 ax-11o 1254 ax-ext 1499 |
| This theorem depends on definitions: df-bi 145 df-an 223 df-ex 1016 df-sb 1208 df-clab 1505 df-cleq 1510 df-clel 1513 df-v 1857 df-dif 2100 df-br 2692 df-sdom 4509 |