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 , 𝑌 ⟩ } )