Metamath Proof Explorer


Theorem ovmpod

Description: Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses ovmpod.1 φ F = x C , y D R
ovmpod.2 φ x = A y = B R = S
ovmpod.3 φ A C
ovmpod.4 φ B D
ovmpod.5 φ S X
Assertion ovmpod φ A F B = S

Proof

Step Hyp Ref Expression
1 ovmpod.1 φ F = x C , y D R
2 ovmpod.2 φ x = A y = B R = S
3 ovmpod.3 φ A C
4 ovmpod.4 φ B D
5 ovmpod.5 φ S X
6 eqidd φ x = A D = D
7 1 2 6 3 4 5 ovmpodx φ A F B = S