![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reldom | Structured version Visualization version Unicode version |
Description: Dominance is a relation. (Contributed by NM, 28-Mar-1998.) |
Ref | Expression |
---|---|
reldom |
![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dom 7602 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | relopabi 4981 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4541 ax-nul 4550 ax-pr 4656 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-opab 4478 df-xp 4862 df-rel 4863 df-dom 7602 |
This theorem is referenced by: relsdom 7607 brdomg 7610 brdomi 7611 domtr 7653 undom 7691 xpdom2 7698 xpdom1g 7700 domunsncan 7703 sbth 7723 sbthcl 7725 dom0 7731 fodomr 7754 pwdom 7755 domssex 7764 mapdom1 7768 mapdom2 7774 fineqv 7818 infsdomnn 7863 infn0 7864 elharval 8109 harword 8111 domwdom 8120 unxpwdom 8135 infdifsn 8193 infdiffi 8194 ac10ct 8496 iunfictbso 8576 cdadom1 8647 cdainf 8653 infcda1 8654 pwcdaidm 8656 cdalepw 8657 unctb 8666 infcdaabs 8667 infunabs 8668 infpss 8678 infmap2 8679 fictb 8706 infpssALT 8774 fin34 8851 ttukeylem1 8970 fodomb 8985 wdomac 8986 brdom3 8987 iundom2g 8996 iundom 8998 infxpidm 9018 iunctb 9030 gchdomtri 9085 pwfseq 9120 pwxpndom2 9121 pwxpndom 9122 pwcdandom 9123 gchpwdom 9126 gchaclem 9134 reexALT 11330 hashdomi 12597 cctop 20076 1stcrestlem 20522 2ndcdisj2 20527 dis2ndc 20530 hauspwdom 20571 ufilen 21000 ovoliunnul 22515 uniiccdif 22591 ovoliunnfl 32028 voliunnfl 32030 volsupnfl 32031 nnfoctb 37422 meadjiun 38409 caragenunicl 38453 |
Copyright terms: Public domain | W3C validator |