reldom - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem reldom 4355

Description: Dominance is a relation.

**Assertion**
Ref	Expression
reldom

**Proof of Theorem reldom**
Step	Hyp	Ref	Expression
1		relopab 3256	. 2
2		df-dom 4352	. . 3
3	2	releqi 3234	. 2
4	1, 3	mpbir 190	1

Colors of variables: wff set class

Syntax hints:

wex 977

copab 2656

wrel 3165

wf1 3169

cdom 4349

This theorem is referenced by: relsdom 4356 brdomg 4358 domtr 4396 xpdom2 4422 xpdom1 4423 sbth 4437 sbthcl 4439 fodomr 4463 infsdomnn 4511 alephsucdom 4852 unctb 7519

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-sep 2693 ax-pow 2732 ax-pr 2769

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-v 1803 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-nul 2271 df-pw 2392 df-sn 2402 df-pr 2403 df-op 2406 df-opab 2657 df-xp 3174 df-rel 3175 df-dom 4352