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 i^i B ) C_ ( dom A i^i dom B )

Proof

Step Hyp Ref Expression
1 19.40 
 |-  ( E. y ( <. x , y >. e. A /\ <. x , y >. e. B ) -> ( E. y <. x , y >. e. A /\ E. y <. x , y >. e. B ) )
2 vex 
 |-  x e. _V
3 2 eldm2 
 |-  ( x e. dom ( A i^i B ) <-> E. y <. x , y >. e. ( A i^i B ) )
4 elin 
 |-  ( <. x , y >. e. ( A i^i B ) <-> ( <. x , y >. e. A /\ <. x , y >. e. B ) )
5 4 exbii 
 |-  ( E. y <. x , y >. e. ( A i^i B ) <-> E. y ( <. x , y >. e. A /\ <. x , y >. e. B ) )
6 3 5 bitri 
 |-  ( x e. dom ( A i^i B ) <-> E. y ( <. x , y >. e. A /\ <. x , y >. e. B ) )
7 elin 
 |-  ( x e. ( dom A i^i dom B ) <-> ( x e. dom A /\ x e. dom B ) )
8 2 eldm2 
 |-  ( x e. dom A <-> E. y <. x , y >. e. A )
9 2 eldm2 
 |-  ( x e. dom B <-> E. y <. x , y >. e. B )
10 8 9 anbi12i 
 |-  ( ( x e. dom A /\ x e. dom B ) <-> ( E. y <. x , y >. e. A /\ E. y <. x , y >. e. B ) )
11 7 10 bitri 
 |-  ( x e. ( dom A i^i dom B ) <-> ( E. y <. x , y >. e. A /\ E. y <. x , y >. e. B ) )
12 1 6 11 3imtr4i 
 |-  ( x e. dom ( A i^i B ) -> x e. ( dom A i^i dom B ) )
13 12 ssriv 
 |-  dom ( A i^i B ) C_ ( dom A i^i dom B )