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	⊢ ( 𝐹 ‘ 𝐴 ) = ∪ { 𝑥 ∣ ( 𝐹 “ { 𝐴 } ) = { 𝑥 } }

Proof

Step	Hyp	Ref	Expression
1		dffv3	⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑦 𝑦 ∈ ( 𝐹 “ { 𝐴 } ) )
2		df-iota	⊢ ( ℩ 𝑦 𝑦 ∈ ( 𝐹 “ { 𝐴 } ) ) = ∪ { 𝑥 ∣ { 𝑦 ∣ 𝑦 ∈ ( 𝐹 “ { 𝐴 } ) } = { 𝑥 } }
3		abid2	⊢ { 𝑦 ∣ 𝑦 ∈ ( 𝐹 “ { 𝐴 } ) } = ( 𝐹 “ { 𝐴 } )
4	3	eqeq1i	⊢ ( { 𝑦 ∣ 𝑦 ∈ ( 𝐹 “ { 𝐴 } ) } = { 𝑥 } ↔ ( 𝐹 “ { 𝐴 } ) = { 𝑥 } )
5	4	abbii	⊢ { 𝑥 ∣ { 𝑦 ∣ 𝑦 ∈ ( 𝐹 “ { 𝐴 } ) } = { 𝑥 } } = { 𝑥 ∣ ( 𝐹 “ { 𝐴 } ) = { 𝑥 } }
6	5	unieqi	⊢ ∪ { 𝑥 ∣ { 𝑦 ∣ 𝑦 ∈ ( 𝐹 “ { 𝐴 } ) } = { 𝑥 } } = ∪ { 𝑥 ∣ ( 𝐹 “ { 𝐴 } ) = { 𝑥 } }
7	1 2 6	3eqtri	⊢ ( 𝐹 ‘ 𝐴 ) = ∪ { 𝑥 ∣ ( 𝐹 “ { 𝐴 } ) = { 𝑥 } }