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

Metamath Proof Explorer

Theorem dmres

Description: The domain of a restriction. Exercise 14 of TakeutiZaring p. 25. (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion dmres 
|- dom ( A |` B ) = ( B i^i dom A )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 eldm2 
 |-  ( x e. dom ( A |` B ) <-> E. y <. x , y >. e. ( A |` B ) )
3 19.42v 
 |-  ( E. y ( x e. B /\ <. x , y >. e. A ) <-> ( x e. B /\ E. y <. x , y >. e. A ) )
4 vex 
 |-  y e. _V
5 4 opelresi 
 |-  ( <. x , y >. e. ( A |` B ) <-> ( x e. B /\ <. x , y >. e. A ) )
6 5 exbii 
 |-  ( E. y <. x , y >. e. ( A |` B ) <-> E. y ( x e. B /\ <. x , y >. e. A ) )
7 1 eldm2 
 |-  ( x e. dom A <-> E. y <. x , y >. e. A )
8 7 anbi2i 
 |-  ( ( x e. B /\ x e. dom A ) <-> ( x e. B /\ E. y <. x , y >. e. A ) )
9 3 6 8 3bitr4i 
 |-  ( E. y <. x , y >. e. ( A |` B ) <-> ( x e. B /\ x e. dom A ) )
10 2 9 bitr2i 
 |-  ( ( x e. B /\ x e. dom A ) <-> x e. dom ( A |` B ) )
11 10 ineqri 
 |-  ( B i^i dom A ) = dom ( A |` B )
12 11 eqcomi 
 |-  dom ( A |` B ) = ( B i^i dom A )