Metamath Proof Explorer


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 >. } )