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 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 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 , 𝑌 ⟩ } )