Metamath Proof Explorer


Theorem fvmpt3

Description: Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Hypotheses fvmpt3.a x = A B = C
fvmpt3.b F = x D B
fvmpt3.c x D B V
Assertion fvmpt3 A D F A = C

Proof

Step Hyp Ref Expression
1 fvmpt3.a x = A B = C
2 fvmpt3.b F = x D B
3 fvmpt3.c x D B V
4 1 eleq1d x = A B V C V
5 4 3 vtoclga A D C V
6 1 2 fvmptg A D C V F A = C
7 5 6 mpdan A D F A = C