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

Metamath Proof Explorer

Theorem dffv4

Proof