This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fv2

Description: Alternate definition of function value. Definition 10.11 of Quine p. 68. (Contributed by NM, 30-Apr-2004) (Proof shortened by Andrew Salmon, 17-Sep-2011) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	fv2	⊢ ( 𝐹 ‘ 𝐴 ) = ∪ { 𝑥 ∣ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) }

Proof

Step	Hyp	Ref	Expression
1		df-fv	⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑦 𝐴 𝐹 𝑦 )
2		dfiota2	⊢ ( ℩ 𝑦 𝐴 𝐹 𝑦 ) = ∪ { 𝑥 ∣ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) }
3	1 2	eqtri	⊢ ( 𝐹 ‘ 𝐴 ) = ∪ { 𝑥 ∣ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) }