Metamath Proof Explorer

Theorem dfafv2

Description: Alternative definition of ( F ''' A ) using ( FA ) directly. (Contributed by Alexander van der Vekens, 22-Jul-2017) (Revised by AV, 25-Aug-2022)

Ref Expression
Assertion dfafv2 ⊢ F ''' A = if F defAt A F ⁡ A V

Proof

Step Hyp Ref Expression
1 df-fv ⊢ F ⁡ A = ι x | A F x
2 simprr ⊢ ⊤ ∧ A ∈ dom ⁡ F ∧ ∃! x A F x → ∃! x A F x
3 reuaiotaiota ⊢ ∃! x A F x ↔ ι x | A F x = ι
4 2 3 sylib ⊢ ⊤ ∧ A ∈ dom ⁡ F ∧ ∃! x A F x → ι x | A F x = ι
5 1 4 syl5eq ⊢ ⊤ ∧ A ∈ dom ⁡ F ∧ ∃! x A F x → F ⁡ A = ι
6 eubrdm ⊢ ∃! x A F x → A ∈ dom ⁡ F
7 6 ancri ⊢ ∃! x A F x → A ∈ dom ⁡ F ∧ ∃! x A F x
8 7 con3i ⊢ ¬ A ∈ dom ⁡ F ∧ ∃! x A F x → ¬ ∃! x A F x
9 8 adantl ⊢ ⊤ ∧ ¬ A ∈ dom ⁡ F ∧ ∃! x A F x → ¬ ∃! x A F x
10 aiotavb ⊢ ¬ ∃! x A F x ↔ ι = V
11 9 10 sylib ⊢ ⊤ ∧ ¬ A ∈ dom ⁡ F ∧ ∃! x A F x → ι = V
12 11 eqcomd ⊢ ⊤ ∧ ¬ A ∈ dom ⁡ F ∧ ∃! x A F x → V = ι
13 5 12 ifeqda ⊢ ⊤ → if A ∈ dom ⁡ F ∧ ∃! x A F x F ⁡ A V = ι
14 13 mptru ⊢ if A ∈ dom ⁡ F ∧ ∃! x A F x F ⁡ A V = ι
15 dfdfat2 ⊢ F defAt A ↔ A ∈ dom ⁡ F ∧ ∃! x A F x
16 ifbi ⊢ F defAt A ↔ A ∈ dom ⁡ F ∧ ∃! x A F x → if F defAt A F ⁡ A V = if A ∈ dom ⁡ F ∧ ∃! x A F x F ⁡ A V
17 15 16 ax-mp ⊢ if F defAt A F ⁡ A V = if A ∈ dom ⁡ F ∧ ∃! x A F x F ⁡ A V
18 df-afv ⊢ F ''' A = ι
19 14 17 18 3eqtr4ri ⊢ F ''' A = if F defAt A F ⁡ A V