Theorem xpsfval

Description: The value of the function appearing in xpsval . (Contributed by Mario Carneiro, 15-Aug-2015)

	Ref	Expression
Hypothesis	xpsff1o.f	|- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } )
Assertion	xpsfval	|- ( ( X e. A /\ Y e. B ) -> ( X F Y ) = { <. (/) , X >. , <. 1o , Y >. } )

Proof

Step	Hyp	Ref	Expression
1		xpsff1o.f	|- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } )
2		simpl	|- ( ( x = X /\ y = Y ) -> x = X )
3	2	opeq2d	|- ( ( x = X /\ y = Y ) -> <. (/) , x >. = <. (/) , X >. )
4		simpr	|- ( ( x = X /\ y = Y ) -> y = Y )
5	4	opeq2d	|- ( ( x = X /\ y = Y ) -> <. 1o , y >. = <. 1o , Y >. )
6	3 5	preq12d	|- ( ( x = X /\ y = Y ) -> { <. (/) , x >. , <. 1o , y >. } = { <. (/) , X >. , <. 1o , Y >. } )
7		prex	|- { <. (/) , X >. , <. 1o , Y >. } e. _V
8	6 1 7	ovmpoa	|- ( ( X e. A /\ Y e. B ) -> ( X F Y ) = { <. (/) , X >. , <. 1o , Y >. } )