This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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