Theorem ovmpoga

Description: Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013)

	Ref	Expression
Hypotheses	ovmpoga.1	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑅 = 𝑆 )
	ovmpoga.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
Assertion	ovmpoga	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		ovmpoga.1	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑅 = 𝑆 )
2		ovmpoga.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
3		elex	⊢ ( 𝑆 ∈ 𝐻 → 𝑆 ∈ V )
4	2	a1i	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V ) → 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) )
5	1	adantl	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V ) ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 = 𝑆 )
6		simp1	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V ) → 𝐴 ∈ 𝐶 )
7		simp2	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V ) → 𝐵 ∈ 𝐷 )
8		simp3	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V ) → 𝑆 ∈ V )
9	4 5 6 7 8	ovmpod	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )
10	3 9	syl3an3	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )