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

Theorem funfvex 5084
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 4804 . 2 (𝐹A) = (℩yA𝐹y)
2 funfveu 5080 . . 3 ((Fun 𝐹 A dom 𝐹) → ∃!y A𝐹y)
3 euiotaex 4777 . . 3 (∃!y A𝐹y → (℩yA𝐹y) V)
42, 3syl 14 . 2 ((Fun 𝐹 A dom 𝐹) → (℩yA𝐹y) V)
51, 4syl5eqel 2106 1 ((Fun 𝐹 A dom 𝐹) → (𝐹A) V)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1375  ∃!weu 1881  Vcvv 2533   class class class wbr 3716  dom cdm 4238  cio 4759  Fun wfun 4790  cfv 4796
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 1315  ax-7 1316  ax-gen 1317  ax-ie1 1362  ax-ie2 1363  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 2004  ax-sep 3827  ax-pow 3879  ax-pr 3896
This theorem depends on definitions:  df-bi 110  df-3an 877  df-tru 1231  df-nf 1329  df-sb 1628  df-eu 1884  df-mo 1885  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ral 2287  df-rex 2288  df-v 2535  df-sbc 2740  df-un 2900  df-in 2902  df-ss 2909  df-pw 3313  df-sn 3333  df-pr 3334  df-op 3336  df-uni 3533  df-br 3717  df-opab 3771  df-id 3983  df-cnv 4246  df-co 4247  df-dm 4248  df-iota 4761  df-fun 4798  df-fv 4804
This theorem is referenced by:  fnbrfvb  5106  fvelrnb  5113  funimass4  5116  fvelimab  5121  fniinfv  5123  funfvdm  5128  dmfco  5133  fvco2  5134  eqfnfv  5157  fndmdif  5164  fndmin  5166  fvimacnvi  5173  fvimacnv  5174  funconstss  5177  fniniseg  5179  fniniseg2  5181  fnniniseg2  5182  rexsupp  5183  fvelrn  5190  rexrn  5196  ralrn  5197  dff3im  5204  fmptco  5222  fsn2  5229  fnressn  5241  resfunexg  5274  eufnfv  5281  funfvima3  5284  rexima  5286  ralima  5287  fniunfv  5293  elunirn  5297  dff13  5299  foeqcnvco  5322  f1eqcocnv  5323  isocnv2  5344  isoini  5349  f1oiso  5357  fnovex  5431  suppssof1  5617  offveqb  5619  1stexg  5683  2ndexg  5684  smoiso  5804  rdgruledefgg  5847  rdgi0g  5851  rdgivallem  5853  rdgisuc2  5858  rdg0  5861  frecabex  5865  frectfr  5866
  Copyright terms: Public domain W3C validator