Metamath Proof Explorer

Theorem dmin

Description: The domain of an intersection is included in the intersection of the domains. Theorem 6 of Suppes p. 60. (Contributed by NM, 15-Sep-2004)

		Ref	Expression
	Assertion	dmin	$⊢ dom (A \cap B) \subseteq dom A \cap dom B$

Proof

Step	Hyp	Ref	Expression
1		19.40	$⊢ \exists y (⟨x, y⟩ \in A \land ⟨x, y⟩ \in B) \to (\exists y ⟨x, y⟩ \in A \land \exists y ⟨x, y⟩ \in B)$
2		vex	$⊢ x \in V$
3	2	eldm2	$⊢ x \in dom (A \cap B) \leftrightarrow \exists y ⟨x, y⟩ \in (A \cap B)$
4		elin	$⊢ ⟨x, y⟩ \in (A \cap B) \leftrightarrow (⟨x, y⟩ \in A \land ⟨x, y⟩ \in B)$
5	4	exbii	$⊢ \exists y ⟨x, y⟩ \in (A \cap B) \leftrightarrow \exists y (⟨x, y⟩ \in A \land ⟨x, y⟩ \in B)$
6	3 5	bitri	$⊢ x \in dom (A \cap B) \leftrightarrow \exists y (⟨x, y⟩ \in A \land ⟨x, y⟩ \in B)$
7		elin	$⊢ x \in (dom A \cap dom B) \leftrightarrow (x \in dom A \land x \in dom B)$
8	2	eldm2	$⊢ x \in dom A \leftrightarrow \exists y ⟨x, y⟩ \in A$
9	2	eldm2	$⊢ x \in dom B \leftrightarrow \exists y ⟨x, y⟩ \in B$
10	8 9	anbi12i	$⊢ (x \in dom A \land x \in dom B) \leftrightarrow (\exists y ⟨x, y⟩ \in A \land \exists y ⟨x, y⟩ \in B)$
11	7 10	bitri	$⊢ x \in (dom A \cap dom B) \leftrightarrow (\exists y ⟨x, y⟩ \in A \land \exists y ⟨x, y⟩ \in B)$
12	1 6 11	3imtr4i	$⊢ x \in dom (A \cap B) \to x \in (dom A \cap dom B)$
13	12	ssriv	$⊢ dom (A \cap B) \subseteq dom A \cap dom B$