Metamath Proof Explorer


Theorem dffv4

Description: The previous definition of function value, from before the iota operator was introduced. Although based on the idea embodied by Definition 10.2 of Quine p. 65 (see args ), this definition apparently does not appear in the literature. (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion dffv4 FA=x|FA=x

Proof

Step Hyp Ref Expression
1 dffv3 FA=ιy|yFA
2 df-iota ιy|yFA=x|y|yFA=x
3 abid2 y|yFA=FA
4 3 eqeq1i y|yFA=xFA=x
5 4 abbii x|y|yFA=x=x|FA=x
6 5 unieqi x|y|yFA=x=x|FA=x
7 1 2 6 3eqtri FA=x|FA=x