Metamath Proof Explorer

Theorem afv0nbfvbi

Description: The function's value at an argument is an element of a set if and only if the value of the alternative function at this argument is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion afv0nbfvbi ( ∅ ∉ 𝐵 → ( ( 𝐹 ''' 𝐴 ) ∈ 𝐵 ↔ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 afvvfveq ⊢ ( ( 𝐹 ''' 𝐴 ) ∈ 𝐵 → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
2 eleq1 ⊢ ( ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) → ( ( 𝐹 ''' 𝐴 ) ∈ 𝐵 ↔ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )
3 2 biimpd ⊢ ( ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) → ( ( 𝐹 ''' 𝐴 ) ∈ 𝐵 → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )
4 1 3 mpcom ⊢ ( ( 𝐹 ''' 𝐴 ) ∈ 𝐵 → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )
5 elnelne2 ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ∧ ∅ ∉ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ≠ ∅ )
6 5 ancoms ⊢ ( ( ∅ ∉ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ≠ ∅ )
7 fvfundmfvn0 ⊢ ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
8 df-dfat ⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
9 afvfundmfveq ⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
10 8 9 sylbir ⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
11 eleq1 ⊢ ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ''' 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ ( 𝐹 ''' 𝐴 ) ∈ 𝐵 ) )
12 11 eqcoms ⊢ ( ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ ( 𝐹 ''' 𝐴 ) ∈ 𝐵 ) )
13 12 biimpd ⊢ ( ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( 𝐹 ''' 𝐴 ) ∈ 𝐵 ) )
14 6 7 10 13 4syl ⊢ ( ( ∅ ∉ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( 𝐹 ''' 𝐴 ) ∈ 𝐵 ) )
15 14 ex ⊢ ( ∅ ∉ 𝐵 → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( 𝐹 ''' 𝐴 ) ∈ 𝐵 ) ) )
16 15 pm2.43d ⊢ ( ∅ ∉ 𝐵 → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( 𝐹 ''' 𝐴 ) ∈ 𝐵 ) )
17 4 16 impbid2 ⊢ ( ∅ ∉ 𝐵 → ( ( 𝐹 ''' 𝐴 ) ∈ 𝐵 ↔ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )