Metamath Proof Explorer


Theorem afv2fv0

Description: If the function's value at an argument is the empty set, then the alternate function value at this argument is the empty set or undefined. (Contributed by AV, 3-Sep-2022)

Ref Expression
Assertion afv2fv0 FA=F''''A=F''''AranF

Proof

Step Hyp Ref Expression
1 ioran ¬F''''A=F''''AranF¬F''''A=¬F''''AranF
2 nnel ¬F''''AranFF''''AranF
3 afv2rnfveq F''''AranFF''''A=FA
4 2 3 sylbi ¬F''''AranFF''''A=FA
5 4 eqeq1d ¬F''''AranFF''''A=FA=
6 5 notbid ¬F''''AranF¬F''''A=¬FA=
7 6 biimpac ¬F''''A=¬F''''AranF¬FA=
8 1 7 sylbi ¬F''''A=F''''AranF¬FA=
9 8 con4i FA=F''''A=F''''AranF