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

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 ∩ B ⊆ dom ⁡ A ∩ dom ⁡ B

Proof

Step Hyp Ref Expression
1 19.40 ⊢ ∃ y x y ∈ A ∧ x y ∈ B → ∃ y x y ∈ A ∧ ∃ y x y ∈ B
2 vex ⊢ x ∈ V
3 2 eldm2 ⊢ x ∈ dom ⁡ A ∩ B ↔ ∃ y x y ∈ A ∩ B
4 elin ⊢ x y ∈ A ∩ B ↔ x y ∈ A ∧ x y ∈ B
5 4 exbii ⊢ ∃ y x y ∈ A ∩ B ↔ ∃ y x y ∈ A ∧ x y ∈ B
6 3 5 bitri ⊢ x ∈ dom ⁡ A ∩ B ↔ ∃ y x y ∈ A ∧ x y ∈ B
7 elin ⊢ x ∈ dom ⁡ A ∩ dom ⁡ B ↔ x ∈ dom ⁡ A ∧ x ∈ dom ⁡ B
8 2 eldm2 ⊢ x ∈ dom ⁡ A ↔ ∃ y x y ∈ A
9 2 eldm2 ⊢ x ∈ dom ⁡ B ↔ ∃ y x y ∈ B
10 8 9 anbi12i ⊢ x ∈ dom ⁡ A ∧ x ∈ dom ⁡ B ↔ ∃ y x y ∈ A ∧ ∃ y x y ∈ B
11 7 10 bitri ⊢ x ∈ dom ⁡ A ∩ dom ⁡ B ↔ ∃ y x y ∈ A ∧ ∃ y x y ∈ B
12 1 6 11 3imtr4i ⊢ x ∈ dom ⁡ A ∩ B → x ∈ dom ⁡ A ∩ dom ⁡ B
13 12 ssriv ⊢ dom ⁡ A ∩ B ⊆ dom ⁡ A ∩ dom ⁡ B