Theorem mpoxopoveqd

Description: Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, deduction version. (Contributed by Alexander van der Vekens, 11-Oct-2017)

	Ref	Expression
Hypotheses	mpoxopoveq.f	|- F = ( x e. _V , y e. ( 1st ` x ) |-> { n e. ( 1st ` x ) | ph } )
	mpoxopoveqd.1	|- ( ps -> ( V e. X /\ W e. Y ) )
	mpoxopoveqd.2	|- ( ( ps /\ -. K e. V ) -> { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } = (/) )
Assertion	mpoxopoveqd	|- ( ps -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )

Proof

Step	Hyp	Ref	Expression
1		mpoxopoveq.f	|- F = ( x e. _V , y e. ( 1st ` x ) |-> { n e. ( 1st ` x ) | ph } )
2		mpoxopoveqd.1	|- ( ps -> ( V e. X /\ W e. Y ) )
3		mpoxopoveqd.2	|- ( ( ps /\ -. K e. V ) -> { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } = (/) )
4	1	mpoxopoveq	|- ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )
5	4	ex	|- ( ( V e. X /\ W e. Y ) -> ( K e. V -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } ) )
6	5 2	syl11	|- ( K e. V -> ( ps -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } ) )
7		df-nel	|- ( K e/ V <-> -. K e. V )
8	1	mpoxopynvov0	|- ( K e/ V -> ( <. V , W >. F K ) = (/) )
9	7 8	sylbir	|- ( -. K e. V -> ( <. V , W >. F K ) = (/) )
10	9	adantr	|- ( ( -. K e. V /\ ps ) -> ( <. V , W >. F K ) = (/) )
11	3	eqcomd	|- ( ( ps /\ -. K e. V ) -> (/) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )
12	11	ancoms	|- ( ( -. K e. V /\ ps ) -> (/) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )
13	10 12	eqtrd	|- ( ( -. K e. V /\ ps ) -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )
14	13	ex	|- ( -. K e. V -> ( ps -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } ) )
15	6 14	pm2.61i	|- ( ps -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )