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	syl6bi	|- ( 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 ) )