Theorem dmiin

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

	Ref	Expression
Assertion	dmiin	|- dom |^|_ x e. A B C_ |^|_ x e. A dom B

Proof

Step	Hyp	Ref	Expression
1		nfii1	|- F/_ x |^|_ x e. A B
2	1	nfdm	|- F/_ x dom |^|_ x e. A B
3	2	ssiinf	|- ( dom |^|_ x e. A B C_ |^|_ x e. A dom B <-> A. x e. A dom |^|_ x e. A B C_ dom B )
4		iinss2	|- ( x e. A -> |^|_ x e. A B C_ B )
5		dmss	|- ( |^|_ x e. A B C_ B -> dom |^|_ x e. A B C_ dom B )
6	4 5	syl	|- ( x e. A -> dom |^|_ x e. A B C_ dom B )
7	3 6	mprgbir	|- dom |^|_ x e. A B C_ |^|_ x e. A dom B