Theorem dffv3

Description: A definition of function value in terms of iota. (Contributed by Scott Fenton, 19-Feb-2013)

	Ref	Expression
Assertion	dffv3	⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		df-fv	⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 )
2		elimasng	⊢ ( ( 𝐴 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ) )
3		df-br	⊢ ( 𝐴 𝐹 𝑥 ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 )
4	2 3	bitr4di	⊢ ( ( 𝐴 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ 𝐴 𝐹 𝑥 ) )
5	4	elvd	⊢ ( 𝐴 ∈ V → ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ 𝐴 𝐹 𝑥 ) )
6	5	iotabidv	⊢ ( 𝐴 ∈ V → ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 ) )
7	1 6	eqtr4id	⊢ ( 𝐴 ∈ V → ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ) )
8		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ )
9		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
10	9	biimpi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
11	10	imaeq2d	⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 “ { 𝐴 } ) = ( 𝐹 “ ∅ ) )
12		ima0	⊢ ( 𝐹 “ ∅ ) = ∅
13	11 12	eqtrdi	⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 “ { 𝐴 } ) = ∅ )
14	13	eleq2d	⊢ ( ¬ 𝐴 ∈ V → ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ 𝑥 ∈ ∅ ) )
15	14	iotabidv	⊢ ( ¬ 𝐴 ∈ V → ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ) = ( ℩ 𝑥 𝑥 ∈ ∅ ) )
16		noel	⊢ ¬ 𝑥 ∈ ∅
17	16	nex	⊢ ¬ ∃ 𝑥 𝑥 ∈ ∅
18		euex	⊢ ( ∃! 𝑥 𝑥 ∈ ∅ → ∃ 𝑥 𝑥 ∈ ∅ )
19	17 18	mto	⊢ ¬ ∃! 𝑥 𝑥 ∈ ∅
20		iotanul	⊢ ( ¬ ∃! 𝑥 𝑥 ∈ ∅ → ( ℩ 𝑥 𝑥 ∈ ∅ ) = ∅ )
21	19 20	ax-mp	⊢ ( ℩ 𝑥 𝑥 ∈ ∅ ) = ∅
22	15 21	eqtrdi	⊢ ( ¬ 𝐴 ∈ V → ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ) = ∅ )
23	8 22	eqtr4d	⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ) )
24	7 23	pm2.61i	⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) )