Theorem cnvresima

Description: An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009)

	Ref	Expression
Assertion	cnvresima	|- ( `' ( F |` A ) " B ) = ( ( `' F " B ) i^i A )

Proof

Step	Hyp	Ref	Expression
1		19.41v	|- ( E. s ( ( s e. B /\ <. s , t >. e. `' F ) /\ t e. A ) <-> ( E. s ( s e. B /\ <. s , t >. e. `' F ) /\ t e. A ) )
2		vex	|- s e. _V
3	2	opelresi	|- ( <. t , s >. e. ( F |` A ) <-> ( t e. A /\ <. t , s >. e. F ) )
4		vex	|- t e. _V
5	2 4	opelcnv	|- ( <. s , t >. e. `' ( F |` A ) <-> <. t , s >. e. ( F |` A ) )
6	2 4	opelcnv	|- ( <. s , t >. e. `' F <-> <. t , s >. e. F )
7	6	anbi2ci	|- ( ( <. s , t >. e. `' F /\ t e. A ) <-> ( t e. A /\ <. t , s >. e. F ) )
8	3 5 7	3bitr4i	|- ( <. s , t >. e. `' ( F |` A ) <-> ( <. s , t >. e. `' F /\ t e. A ) )
9	8	bianass	|- ( ( s e. B /\ <. s , t >. e. `' ( F |` A ) ) <-> ( ( s e. B /\ <. s , t >. e. `' F ) /\ t e. A ) )
10	9	exbii	|- ( E. s ( s e. B /\ <. s , t >. e. `' ( F |` A ) ) <-> E. s ( ( s e. B /\ <. s , t >. e. `' F ) /\ t e. A ) )
11	4	elima3	|- ( t e. ( `' F " B ) <-> E. s ( s e. B /\ <. s , t >. e. `' F ) )
12	11	anbi1i	|- ( ( t e. ( `' F " B ) /\ t e. A ) <-> ( E. s ( s e. B /\ <. s , t >. e. `' F ) /\ t e. A ) )
13	1 10 12	3bitr4i	|- ( E. s ( s e. B /\ <. s , t >. e. `' ( F |` A ) ) <-> ( t e. ( `' F " B ) /\ t e. A ) )
14	4	elima3	|- ( t e. ( `' ( F |` A ) " B ) <-> E. s ( s e. B /\ <. s , t >. e. `' ( F |` A ) ) )
15		elin	|- ( t e. ( ( `' F " B ) i^i A ) <-> ( t e. ( `' F " B ) /\ t e. A ) )
16	13 14 15	3bitr4i	|- ( t e. ( `' ( F |` A ) " B ) <-> t e. ( ( `' F " B ) i^i A ) )
17	16	eqriv	|- ( `' ( F |` A ) " B ) = ( ( `' F " B ) i^i A )