Theorem dmiin

Description: Domain of an intersection. (Contributed by FL, 15-Oct-2012)

	Ref	Expression
Assertion	dmiin	⊢ dom ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 dom 𝐵

Proof

Step	Hyp	Ref	Expression
1		nfii1	⊢ Ⅎ 𝑥 ∩ 𝑥 ∈ 𝐴 𝐵
2	1	nfdm	⊢ Ⅎ 𝑥 dom ∩ 𝑥 ∈ 𝐴 𝐵
3	2	ssiinf	⊢ ( dom ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 dom 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 dom ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ dom 𝐵 )
4		iinss2	⊢ ( 𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 )
5		dmss	⊢ ( ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 → dom ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ dom 𝐵 )
6	4 5	syl	⊢ ( 𝑥 ∈ 𝐴 → dom ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ dom 𝐵 )
7	3 6	mprgbir	⊢ dom ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 dom 𝐵