Theorem ovmpo

Description: Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 16-May-1995) (Revised by David Abernethy, 19-Jun-2012)

	Ref	Expression
Hypotheses	ovmpog.1	⊢ ( 𝑥 = 𝐴 → 𝑅 = 𝐺 )
	ovmpog.2	⊢ ( 𝑦 = 𝐵 → 𝐺 = 𝑆 )
	ovmpog.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
	ovmpo.4	⊢ 𝑆 ∈ V
Assertion	ovmpo	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		ovmpog.1	⊢ ( 𝑥 = 𝐴 → 𝑅 = 𝐺 )
2		ovmpog.2	⊢ ( 𝑦 = 𝐵 → 𝐺 = 𝑆 )
3		ovmpog.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
4		ovmpo.4	⊢ 𝑆 ∈ V
5	1 2 3	ovmpog	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )
6	4 5	mp3an3	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 )