Theorem funfvex 5192

Description: The value of a function exists. A special case of Corollary 6.13 of [TakeutiZaring] p. 27. (Contributed by Jim Kingdon, 29-Dec-2018.)

Assertion

Ref	Expression
funfvex	⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ V)

Proof of Theorem funfvex

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-fv 4910	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		funfveu 5188	. . 3 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ∃!𝑦 𝐴𝐹𝑦)
3		euiotaex 4883	. . 3 ⊢ (∃!𝑦 𝐴𝐹𝑦 → (℩𝑦𝐴𝐹𝑦) ∈ V)
4	2, 3	syl 14	. 2 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (℩𝑦𝐴𝐹𝑦) ∈ V)
5	1, 4	syl5eqel 2124	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ V)

Syntax hints:   → wi 4   ∧ wa 97   ∈ wcel 1393  ∃!weu 1900  Vcvv 2557   class class class wbr 3764  dom cdm 4345  ℩cio 4865  Fun wfun 4896  ‘cfv 4902

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-sbc 2765  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-opab 3819  df-id 4030  df-cnv 4353  df-co 4354  df-dm 4355  df-iota 4867  df-fun 4904  df-fv 4910

This theorem is referenced by:  fnbrfvb  5214  fvelrnb  5221  funimass4  5224  fvelimab  5229  fniinfv  5231  funfvdm  5236  dmfco  5241  fvco2  5242  eqfnfv  5265  fndmdif  5272  fndmin  5274  fvimacnvi  5281  fvimacnv  5282  funconstss  5285  fniniseg  5287  fniniseg2  5289  fnniniseg2  5290  rexsupp  5291  fvelrn  5298  rexrn  5304  ralrn  5305  dff3im  5312  fmptco  5330  fsn2  5337  fnressn  5349  resfunexg  5382  eufnfv  5389  funfvima3  5392  rexima  5394  ralima  5395  fniunfv  5401  elunirn  5405  dff13  5407  foeqcnvco  5430  f1eqcocnv  5431  isocnv2  5452  isoini  5457  f1oiso  5465  fnovex  5538  suppssof1  5728  offveqb  5730  1stexg  5794  2ndexg  5795  smoiso  5917  rdgtfr  5961  rdgruledefgg  5962  rdgivallem  5968  frectfr  5985  frecrdg  5992  freccl  5993  en1  6279  fundmen  6286  ordiso2  6357  climshft2  9827