Theorem afv2eu 47187

Description: The value of a function at a unique point, analogous to fveu 6895. (Contributed by AV, 5-Sep-2022.)

Assertion

Ref	Expression
afv2eu	⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐹''''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥})

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Proof of Theorem afv2eu

Step	Hyp	Ref	Expression
1		eubrv 46984	. 2 ⊢ (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ V)
2		euex 2574	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
3		eldmg 5911	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
4	2, 3	syl5ibrcom 247	. . . 4 ⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐴 ∈ V → 𝐴 ∈ dom 𝐹))
5	4	impcom 407	. . 3 ⊢ ((𝐴 ∈ V ∧ ∃!𝑥 𝐴𝐹𝑥) → 𝐴 ∈ dom 𝐹)
6		dfdfat2 47077	. . . . . . 7 ⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ ∃!𝑥 𝐴𝐹𝑥))
7		dfatafv2iota 47159	. . . . . . . . 9 ⊢ (𝐹 defAt 𝐴 → (𝐹''''𝐴) = (℩𝑥𝐴𝐹𝑥))
8		iotauni 6537	. . . . . . . . 9 ⊢ (∃!𝑥 𝐴𝐹𝑥 → (℩𝑥𝐴𝐹𝑥) = ∪ {𝑥 ∣ 𝐴𝐹𝑥})
9	7, 8	sylan9eq 2794	. . . . . . . 8 ⊢ ((𝐹 defAt 𝐴 ∧ ∃!𝑥 𝐴𝐹𝑥) → (𝐹''''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥})
10	9	ex 412	. . . . . . 7 ⊢ (𝐹 defAt 𝐴 → (∃!𝑥 𝐴𝐹𝑥 → (𝐹''''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥}))
11	6, 10	sylbir 235	. . . . . 6 ⊢ ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑥 𝐴𝐹𝑥) → (∃!𝑥 𝐴𝐹𝑥 → (𝐹''''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥}))
12	11	expcom 413	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐴 ∈ dom 𝐹 → (∃!𝑥 𝐴𝐹𝑥 → (𝐹''''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥})))
13	12	pm2.43a 54	. . . 4 ⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐴 ∈ dom 𝐹 → (𝐹''''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥}))
14	13	adantl 481	. . 3 ⊢ ((𝐴 ∈ V ∧ ∃!𝑥 𝐴𝐹𝑥) → (𝐴 ∈ dom 𝐹 → (𝐹''''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥}))
15	5, 14	mpd 15	. 2 ⊢ ((𝐴 ∈ V ∧ ∃!𝑥 𝐴𝐹𝑥) → (𝐹''''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥})
16	1, 15	mpancom 688	1 ⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐹''''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥})

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536  ∃wex 1775   ∈ wcel 2105  ∃!weu 2565  {cab 2711  Vcvv 3477  ∪ cuni 4911   class class class wbr 5147  dom cdm 5688  ℩cio 6513   defAt wdfat 47065  ''''cafv2 47157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-res 5700  df-iota 6515  df-fun 6564  df-dfat 47068  df-afv2 47158

This theorem is referenced by: (None)