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 ( 𝐴 ∩ 𝐵 ) ⊆ ( dom 𝐴 ∩ dom 𝐵 )

Proof

Step Hyp Ref Expression
1 19.40 ⊢ ( ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ∧ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
2 vex ⊢ 𝑥 ∈ V
3 2 eldm2 ⊢ ( 𝑥 ∈ dom ( 𝐴 ∩ 𝐵 ) ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∩ 𝐵 ) )
4 elin ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
5 4 exbii ⊢ ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∩ 𝐵 ) ↔ ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
6 3 5 bitri ⊢ ( 𝑥 ∈ dom ( 𝐴 ∩ 𝐵 ) ↔ ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
7 elin ⊢ ( 𝑥 ∈ ( dom 𝐴 ∩ dom 𝐵 ) ↔ ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ dom 𝐵 ) )
8 2 eldm2 ⊢ ( 𝑥 ∈ dom 𝐴 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
9 2 eldm2 ⊢ ( 𝑥 ∈ dom 𝐵 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
10 8 9 anbi12i ⊢ ( ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ dom 𝐵 ) ↔ ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ∧ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
11 7 10 bitri ⊢ ( 𝑥 ∈ ( dom 𝐴 ∩ dom 𝐵 ) ↔ ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ∧ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
12 1 6 11 3imtr4i ⊢ ( 𝑥 ∈ dom ( 𝐴 ∩ 𝐵 ) → 𝑥 ∈ ( dom 𝐴 ∩ dom 𝐵 ) )
13 12 ssriv ⊢ dom ( 𝐴 ∩ 𝐵 ) ⊆ ( dom 𝐴 ∩ dom 𝐵 )