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

Metamath Proof Explorer

Theorem dfres3

Description: Alternate definition of restriction. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion dfres3 
|- ( A |` B ) = ( A i^i ( B X. ran A ) )

Proof

Step Hyp Ref Expression
1 df-res 
 |-  ( A |` B ) = ( A i^i ( B X. _V ) )
2 eleq1 
 |-  ( x = <. y , z >. -> ( x e. A <-> <. y , z >. e. A ) )
3 vex 
 |-  z e. _V
4 3 biantru 
 |-  ( y e. B <-> ( y e. B /\ z e. _V ) )
5 vex 
 |-  y e. _V
6 5 3 opelrn 
 |-  ( <. y , z >. e. A -> z e. ran A )
7 6 biantrud 
 |-  ( <. y , z >. e. A -> ( y e. B <-> ( y e. B /\ z e. ran A ) ) )
8 4 7 bitr3id 
 |-  ( <. y , z >. e. A -> ( ( y e. B /\ z e. _V ) <-> ( y e. B /\ z e. ran A ) ) )
9 2 8 biimtrdi 
 |-  ( x = <. y , z >. -> ( x e. A -> ( ( y e. B /\ z e. _V ) <-> ( y e. B /\ z e. ran A ) ) ) )
10 9 com12 
 |-  ( x e. A -> ( x = <. y , z >. -> ( ( y e. B /\ z e. _V ) <-> ( y e. B /\ z e. ran A ) ) ) )
11 10 pm5.32d 
 |-  ( x e. A -> ( ( x = <. y , z >. /\ ( y e. B /\ z e. _V ) ) <-> ( x = <. y , z >. /\ ( y e. B /\ z e. ran A ) ) ) )
12 11 2exbidv 
 |-  ( x e. A -> ( E. y E. z ( x = <. y , z >. /\ ( y e. B /\ z e. _V ) ) <-> E. y E. z ( x = <. y , z >. /\ ( y e. B /\ z e. ran A ) ) ) )
13 elxp 
 |-  ( x e. ( B X. _V ) <-> E. y E. z ( x = <. y , z >. /\ ( y e. B /\ z e. _V ) ) )
14 elxp 
 |-  ( x e. ( B X. ran A ) <-> E. y E. z ( x = <. y , z >. /\ ( y e. B /\ z e. ran A ) ) )
15 12 13 14 3bitr4g 
 |-  ( x e. A -> ( x e. ( B X. _V ) <-> x e. ( B X. ran A ) ) )
16 15 pm5.32i 
 |-  ( ( x e. A /\ x e. ( B X. _V ) ) <-> ( x e. A /\ x e. ( B X. ran A ) ) )
17 elin 
 |-  ( x e. ( A i^i ( B X. ran A ) ) <-> ( x e. A /\ x e. ( B X. ran A ) ) )
18 16 17 bitr4i 
 |-  ( ( x e. A /\ x e. ( B X. _V ) ) <-> x e. ( A i^i ( B X. ran A ) ) )
19 18 ineqri 
 |-  ( A i^i ( B X. _V ) ) = ( A i^i ( B X. ran A ) )
20 1 19 eqtri 
 |-  ( A |` B ) = ( A i^i ( B X. ran A ) )