ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  funfvex Structured version   GIF version

Theorem funfvex 5115
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 𝐹 A dom 𝐹) → (𝐹A) V)

Proof of Theorem funfvex
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 df-fv 4835 . 2 (𝐹A) = (℩yA𝐹y)
2 funfveu 5111 . . 3 ((Fun 𝐹 A dom 𝐹) → ∃!y A𝐹y)
3 euiotaex 4808 . . 3 (∃!y A𝐹y → (℩yA𝐹y) V)
42, 3syl 14 . 2 ((Fun 𝐹 A dom 𝐹) → (℩yA𝐹y) V)
51, 4syl5eqel 2107 1 ((Fun 𝐹 A dom 𝐹) → (𝐹A) V)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1375  ∃!weu 1883  Vcvv 2534   class class class wbr 3737  dom cdm 4270  cio 4790  Fun wfun 4821  cfv 4827
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 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1364  ax-ie2 1365  ax-8 1377  ax-10 1378  ax-11 1379  ax-i12 1380  ax-bnd 1381  ax-4 1382  ax-14 1387  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-i5r 1411  ax-ext 2005  ax-sep 3848  ax-pow 3900  ax-pr 3917
This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1629  df-eu 1886  df-mo 1887  df-clab 2010  df-cleq 2016  df-clel 2019  df-nfc 2150  df-ral 2288  df-rex 2289  df-v 2536  df-sbc 2741  df-un 2898  df-in 2900  df-ss 2907  df-pw 3335  df-sn 3355  df-pr 3356  df-op 3358  df-uni 3554  df-br 3738  df-opab 3792  df-id 4003  df-cnv 4278  df-co 4279  df-dm 4280  df-iota 4792  df-fun 4829  df-fv 4835
This theorem is referenced by:  fnbrfvb  5137  fvelrnb  5144  funimass4  5147  fvelimab  5152  fniinfv  5154  funfvdm  5159  dmfco  5164  fvco2  5165  eqfnfv  5188  fndmdif  5195  fndmin  5197  fvimacnvi  5204  fvimacnv  5205  funconstss  5208  fniniseg  5210  fniniseg2  5212  fnniniseg2  5213  rexsupp  5214  fvelrn  5221  rexrn  5227  ralrn  5228  dff3im  5235  fmptco  5253  fsn2  5260  fnressn  5272  resfunexg  5305  eufnfv  5312  funfvima3  5315  rexima  5317  ralima  5318  fniunfv  5324  elunirn  5328  dff13  5330  foeqcnvco  5353  f1eqcocnv  5354  isocnv2  5375  isoini  5380  f1oiso  5388  fnovex  5460  suppssof1  5648  offveqb  5650  1stexg  5714  2ndexg  5715  smoiso  5834  rdgruledefgg  5877  rdgi0g  5881  rdgivallem  5883  rdg0  5890  frecabex  5894  frectfr  5895
  Copyright terms: Public domain W3C validator