Theorem 0domg

Description: Any set dominates the empty set. (Contributed by NM, 26-Oct-2003) (Revised by Mario Carneiro, 26-Apr-2015) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 29-Nov-2024)

	Ref	Expression
Assertion	0domg	$$⊢A\in V\to \varnothing \preccurlyeq A$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		f1eq1	$$⊢f=\varnothing \to \left(f:\varnothing \underset{1-1}{⟶}A\leftrightarrow \varnothing :\varnothing \underset{1-1}{⟶}A\right)$$
3		f10	$$⊢\varnothing :\varnothing \underset{1-1}{⟶}A$$
4	1 2 3	ceqsexv2d	$$⊢\exists ff:\varnothing \underset{1-1}{⟶}A$$
5		brdom2g	$$⊢\left(\varnothing \in \mathrm{V}\wedge A\in V\right)\to \left(\varnothing \preccurlyeq A\leftrightarrow \exists ff:\varnothing \underset{1-1}{⟶}A\right)$$
6	1 5	mpan	$$⊢A\in V\to \left(\varnothing \preccurlyeq A\leftrightarrow \exists ff:\varnothing \underset{1-1}{⟶}A\right)$$
7	4 6	mpbiri	$$⊢A\in V\to \varnothing \preccurlyeq A$$