Theorem mpoxeldm

Description: If there is an element of the value of an operation given by a maps-to rule, then the first argument is an element of the first component of the domain and the second argument is an element of the second component of the domain depending on the first argument. (Contributed by AV, 25-Oct-2020)

	Ref	Expression
Hypothesis	mpoxeldm.f	|- F = ( x e. C , y e. D |-> R )
Assertion	mpoxeldm	|- ( N e. ( X F Y ) -> ( X e. C /\ Y e. [_ X / x ]_ D ) )

Proof

Step	Hyp	Ref	Expression
1		mpoxeldm.f	|- F = ( x e. C , y e. D |-> R )
2	1	dmmpossx	|- dom F C_ U_ x e. C ( { x } X. D )
3		elfvdm	|- ( N e. ( F ` <. X , Y >. ) -> <. X , Y >. e. dom F )
4		df-ov	|- ( X F Y ) = ( F ` <. X , Y >. )
5	3 4	eleq2s	|- ( N e. ( X F Y ) -> <. X , Y >. e. dom F )
6	2 5	sselid	|- ( N e. ( X F Y ) -> <. X , Y >. e. U_ x e. C ( { x } X. D ) )
7		nfcsb1v	|- F/_ x [_ X / x ]_ D
8		csbeq1a	|- ( x = X -> D = [_ X / x ]_ D )
9	7 8	opeliunxp2f	|- ( <. X , Y >. e. U_ x e. C ( { x } X. D ) <-> ( X e. C /\ Y e. [_ X / x ]_ D ) )
10	6 9	sylib	|- ( N e. ( X F Y ) -> ( X e. C /\ Y e. [_ X / x ]_ D ) )