Theorem domeng

Description: Dominance in terms of equinumerosity, with the sethood requirement expressed as an antecedent. Example 1 of Enderton p. 146. (Contributed by NM, 24-Apr-2004)

	Ref	Expression
Assertion	domeng	$$⊢B\in C\to \left(A\preccurlyeq B\leftrightarrow \exists x\left(A\approx x\wedge x\subseteq B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢y=B\to \left(A\preccurlyeq y\leftrightarrow A\preccurlyeq B\right)$$
2		sseq2	$$⊢y=B\to \left(x\subseteq y\leftrightarrow x\subseteq B\right)$$
3	2	anbi2d	$$⊢y=B\to \left(\left(A\approx x\wedge x\subseteq y\right)\leftrightarrow \left(A\approx x\wedge x\subseteq B\right)\right)$$
4	3	exbidv	$$⊢y=B\to \left(\exists x\left(A\approx x\wedge x\subseteq y\right)\leftrightarrow \exists x\left(A\approx x\wedge x\subseteq B\right)\right)$$
5		vex	$$⊢y\in \mathrm{V}$$
6	5	domen	$$⊢A\preccurlyeq y\leftrightarrow \exists x\left(A\approx x\wedge x\subseteq y\right)$$
7	1 4 6	vtoclbg	$$⊢B\in C\to \left(A\preccurlyeq B\leftrightarrow \exists x\left(A\approx x\wedge x\subseteq B\right)\right)$$