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