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

Theorem funfni 4942
Description: Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.)
Hypothesis
Ref Expression
funfni.1  Fun  F  dom  F
Assertion
Ref Expression
funfni  F  Fn

Proof of Theorem funfni
StepHypRef Expression
1 fnfun 4939 . . 3  F  Fn  Fun  F
21adantr 261 . 2  F  Fn  Fun  F
3 fndm 4941 . . . 4  F  Fn  dom  F
43eleq2d 2104 . . 3  F  Fn  dom  F
54biimpar 281 . 2  F  Fn  dom  F
6 funfni.1 . 2  Fun  F  dom  F
72, 5, 6syl2anc 391 1  F  Fn
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wcel 1390   dom cdm 4288   Fun wfun 4839    Fn wfn 4840
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-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033  df-fn 4848
This theorem is referenced by:  fneu  4946  fnbrfvb  5157  fvelrnb  5164  fvelimab  5172  fniinfv  5174  fvco2  5185  eqfnfv  5208  fndmdif  5215  fndmin  5217  elpreima  5229  fniniseg  5230  fniniseg2  5232  fnniniseg2  5233  rexsupp  5234  fnopfv  5240  fnfvelrn  5242  rexrn  5247  ralrn  5248  fsn2  5280  fnressn  5292  eufnfv  5332  rexima  5337  ralima  5338  fniunfv  5344  dff13  5350  foeqcnvco  5373  f1eqcocnv  5374  isocnv2  5395  isoini  5400  f1oiso  5408  fnovex  5481  suppssof1  5670  offveqb  5672  1stexg  5736  2ndexg  5737  smoiso  5858  rdgruledefgg  5902  rdgivallem  5908  frectfr  5924  frecrdg  5931  freccl  5932  en1  6215
  Copyright terms: Public domain W3C validator