Theorem cnviin

Description: The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012)

	Ref	Expression
Assertion	cnviin	|- ( A =/= (/) -> `' |^|_ x e. A B = |^|_ x e. A `' B )

Proof

Step	Hyp	Ref	Expression
1		relcnv	|- Rel `' |^|_ x e. A B
2		relcnv	|- Rel `' B
3		df-rel	|- ( Rel `' B <-> `' B C_ ( _V X. _V ) )
4	2 3	mpbi	|- `' B C_ ( _V X. _V )
5	4	rgenw	|- A. x e. A `' B C_ ( _V X. _V )
6		r19.2z	|- ( ( A =/= (/) /\ A. x e. A `' B C_ ( _V X. _V ) ) -> E. x e. A `' B C_ ( _V X. _V ) )
7	5 6	mpan2	|- ( A =/= (/) -> E. x e. A `' B C_ ( _V X. _V ) )
8		iinss	|- ( E. x e. A `' B C_ ( _V X. _V ) -> |^|_ x e. A `' B C_ ( _V X. _V ) )
9	7 8	syl	|- ( A =/= (/) -> |^|_ x e. A `' B C_ ( _V X. _V ) )
10		df-rel	|- ( Rel |^|_ x e. A `' B <-> |^|_ x e. A `' B C_ ( _V X. _V ) )
11	9 10	sylibr	|- ( A =/= (/) -> Rel |^|_ x e. A `' B )
12		opex	|- <. b , a >. e. _V
13		eliin	|- ( <. b , a >. e. _V -> ( <. b , a >. e. |^|_ x e. A B <-> A. x e. A <. b , a >. e. B ) )
14	12 13	ax-mp	|- ( <. b , a >. e. |^|_ x e. A B <-> A. x e. A <. b , a >. e. B )
15		vex	|- a e. _V
16		vex	|- b e. _V
17	15 16	opelcnv	|- ( <. a , b >. e. `' |^|_ x e. A B <-> <. b , a >. e. |^|_ x e. A B )
18		opex	|- <. a , b >. e. _V
19		eliin	|- ( <. a , b >. e. _V -> ( <. a , b >. e. |^|_ x e. A `' B <-> A. x e. A <. a , b >. e. `' B ) )
20	18 19	ax-mp	|- ( <. a , b >. e. |^|_ x e. A `' B <-> A. x e. A <. a , b >. e. `' B )
21	15 16	opelcnv	|- ( <. a , b >. e. `' B <-> <. b , a >. e. B )
22	21	ralbii	|- ( A. x e. A <. a , b >. e. `' B <-> A. x e. A <. b , a >. e. B )
23	20 22	bitri	|- ( <. a , b >. e. |^|_ x e. A `' B <-> A. x e. A <. b , a >. e. B )
24	14 17 23	3bitr4i	|- ( <. a , b >. e. `' |^|_ x e. A B <-> <. a , b >. e. |^|_ x e. A `' B )
25	24	eqrelriv	|- ( ( Rel `' |^|_ x e. A B /\ Rel |^|_ x e. A `' B ) -> `' |^|_ x e. A B = |^|_ x e. A `' B )
26	1 11 25	sylancr	|- ( A =/= (/) -> `' |^|_ x e. A B = |^|_ x e. A `' B )