Theorem afv0nbfvbi 47745

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.)

Assertion

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

Proof of Theorem afv0nbfvbi

Step	Hyp	Ref	Expression
1		afvvfveq 47742	. . 3 ⊢ ((𝐹'''𝐴) ∈ 𝐵 → (𝐹'''𝐴) = (𝐹‘𝐴))
2		eleq1 2850	. . . 4 ⊢ ((𝐹'''𝐴) = (𝐹‘𝐴) → ((𝐹'''𝐴) ∈ 𝐵 ↔ (𝐹‘𝐴) ∈ 𝐵))
3	2	biimpd 231	. . 3 ⊢ ((𝐹'''𝐴) = (𝐹‘𝐴) → ((𝐹'''𝐴) ∈ 𝐵 → (𝐹‘𝐴) ∈ 𝐵))
4	1, 3	mpcom 38	. 2 ⊢ ((𝐹'''𝐴) ∈ 𝐵 → (𝐹‘𝐴) ∈ 𝐵)
5		elnelne2 3073	. . . . . 6 ⊢ (((𝐹‘𝐴) ∈ 𝐵 ∧ ∅ ∉ 𝐵) → (𝐹‘𝐴) ≠ ∅)
6	5	ancoms 462	. . . . 5 ⊢ ((∅ ∉ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝐵) → (𝐹‘𝐴) ≠ ∅)
7		fvfundmfvn0 6907	. . . . 5 ⊢ ((𝐹‘𝐴) ≠ ∅ → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
8		df-dfat 47713	. . . . . 6 ⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
9		afvfundmfveq 47732	. . . . . 6 ⊢ (𝐹 defAt 𝐴 → (𝐹'''𝐴) = (𝐹‘𝐴))
10	8, 9	sylbir 237	. . . . 5 ⊢ ((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → (𝐹'''𝐴) = (𝐹‘𝐴))
11		eleq1 2850	. . . . . . 7 ⊢ ((𝐹‘𝐴) = (𝐹'''𝐴) → ((𝐹‘𝐴) ∈ 𝐵 ↔ (𝐹'''𝐴) ∈ 𝐵))
12	11	eqcoms 2770	. . . . . 6 ⊢ ((𝐹'''𝐴) = (𝐹‘𝐴) → ((𝐹‘𝐴) ∈ 𝐵 ↔ (𝐹'''𝐴) ∈ 𝐵))
13	12	biimpd 231	. . . . 5 ⊢ ((𝐹'''𝐴) = (𝐹‘𝐴) → ((𝐹‘𝐴) ∈ 𝐵 → (𝐹'''𝐴) ∈ 𝐵))
14	6, 7, 10, 13	4syl 19	. . . 4 ⊢ ((∅ ∉ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝐵) → ((𝐹‘𝐴) ∈ 𝐵 → (𝐹'''𝐴) ∈ 𝐵))
15	14	ex 416	. . 3 ⊢ (∅ ∉ 𝐵 → ((𝐹‘𝐴) ∈ 𝐵 → ((𝐹‘𝐴) ∈ 𝐵 → (𝐹'''𝐴) ∈ 𝐵)))
16	15	pm2.43d 53	. 2 ⊢ (∅ ∉ 𝐵 → ((𝐹‘𝐴) ∈ 𝐵 → (𝐹'''𝐴) ∈ 𝐵))
17	4, 16	impbid2 228	1 ⊢ (∅ ∉ 𝐵 → ((𝐹'''𝐴) ∈ 𝐵 ↔ (𝐹‘𝐴) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142   ≠ wne 2957   ∉ wnel 3061  ∅c0 4285  {csn 4582  dom cdm 5647   ↾ cres 5649  Fun wfun 6515  ‘cfv 6521   defAt wdfat 47710  '''cafv 47711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4906  df-br 5101  df-opab 5163  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-res 5659  df-iota 6477  df-fun 6523  df-fv 6529  df-aiota 47679  df-dfat 47713  df-afv 47714

This theorem is referenced by:  aov0nbovbi  47789