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

Metamath Proof Explorer

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