This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (A ≼ B \leftrightarrow \exists x (A \approx x \land x \subseteq B))$

Proof

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