![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > brsdom | Unicode version |
Description: Strict dominance
relation, meaning "![]() ![]() |
Ref | Expression |
---|---|
brsdom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sdom 7071 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eleq2i 2468 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-br 4173 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-br 4173 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | df-br 4173 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | notbii 288 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | anbi12i 679 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | eldif 3290 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | bitr4i 244 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 2, 3, 9 | 3bitr4i 269 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: sdomdom 7094 sdomnen 7095 0sdomg 7195 sdomdomtr 7199 domsdomtr 7201 domtriord 7212 canth2 7219 php2 7251 php3 7252 nnsdomo 7260 nnsdomg 7325 card2inf 7479 cardsdomelir 7816 cardsdom2 7831 fidomtri2 7837 cardmin2 7841 alephordi 7911 alephord 7912 isfin4-3 8151 isfin5-2 8227 canthnum 8480 canthwe 8482 canthp1 8485 gchcdaidm 8499 gchxpidm 8500 gchhar 8502 axgroth6 8659 hashsdom 11610 ruc 12797 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 |
This theorem depends on definitions: df-bi 178 df-an 361 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-v 2918 df-dif 3283 df-br 4173 df-sdom 7071 |
Copyright terms: Public domain | W3C validator |