Theorem xpsfval

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

	Ref	Expression
Hypothesis	xpsff1o.f	$$⊢F=\left(x\in A,y\in B⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
Assertion	xpsfval	$$⊢\left(X\in A\wedge Y\in B\right)\to XFY=\left\{⟨\varnothing ,X⟩,⟨1_{𝑜},Y⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		xpsff1o.f	$$⊢F=\left(x\in A,y\in B⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
2		simpl	$$⊢\left(x=X\wedge y=Y\right)\to x=X$$
3	2	opeq2d	$$⊢\left(x=X\wedge y=Y\right)\to ⟨\varnothing ,x⟩=⟨\varnothing ,X⟩$$
4		simpr	$$⊢\left(x=X\wedge y=Y\right)\to y=Y$$
5	4	opeq2d	$$⊢\left(x=X\wedge y=Y\right)\to ⟨1_{𝑜},y⟩=⟨1_{𝑜},Y⟩$$
6	3 5	preq12d	$$⊢\left(x=X\wedge y=Y\right)\to \left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}=\left\{⟨\varnothing ,X⟩,⟨1_{𝑜},Y⟩\right\}$$
7		prex	$$⊢\left\{⟨\varnothing ,X⟩,⟨1_{𝑜},Y⟩\right\}\in \mathrm{V}$$
8	6 1 7	ovmpoa	$$⊢\left(X\in A\wedge Y\in B\right)\to XFY=\left\{⟨\varnothing ,X⟩,⟨1_{𝑜},Y⟩\right\}$$