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 𝐹 = ( 𝑥𝐴 , 𝑦𝐵 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
Assertion xpsfval ( ( 𝑋𝐴𝑌𝐵 ) → ( 𝑋 𝐹 𝑌 ) = { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1o , 𝑌 ⟩ } )

Proof

Step Hyp Ref Expression
1 xpsff1o.f 𝐹 = ( 𝑥𝐴 , 𝑦𝐵 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
2 simpl ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → 𝑥 = 𝑋 )
3 2 opeq2d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ⟨ ∅ , 𝑥 ⟩ = ⟨ ∅ , 𝑋 ⟩ )
4 simpr ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
5 4 opeq2d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ⟨ 1o , 𝑦 ⟩ = ⟨ 1o , 𝑌 ⟩ )
6 3 5 preq12d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } = { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1o , 𝑌 ⟩ } )
7 prex { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1o , 𝑌 ⟩ } ∈ V
8 6 1 7 ovmpoa ( ( 𝑋𝐴𝑌𝐵 ) → ( 𝑋 𝐹 𝑌 ) = { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1o , 𝑌 ⟩ } )