Metamath Proof Explorer


Theorem afv0fv0

Description: If the value of the alternative function at an argument is the empty set, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion afv0fv0 F ''' A = F A =

Proof

Step Hyp Ref Expression
1 0ex V
2 eleq1a V F ''' A = F ''' A V
3 1 2 ax-mp F ''' A = F ''' A V
4 afvvfveq F ''' A V F ''' A = F A
5 eqeq1 F ''' A = F A F ''' A = F A =
6 5 biimpd F ''' A = F A F ''' A = F A =
7 4 6 syl F ''' A V F ''' A = F A =
8 3 7 mpcom F ''' A = F A =