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

Theorem funfni 4921
Description: Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.)
Hypothesis
Ref Expression
funfni.1 ((Fun 𝐹 B dom 𝐹) → φ)
Assertion
Ref Expression
funfni ((𝐹 Fn A B A) → φ)

Proof of Theorem funfni
StepHypRef Expression
1 fnfun 4918 . . 3 (𝐹 Fn A → Fun 𝐹)
21adantr 261 . 2 ((𝐹 Fn A B A) → Fun 𝐹)
3 fndm 4920 . . . 4 (𝐹 Fn A → dom 𝐹 = A)
43eleq2d 2085 . . 3 (𝐹 Fn A → (B dom 𝐹B A))
54biimpar 281 . 2 ((𝐹 Fn A B A) → B dom 𝐹)
6 funfni.1 . 2 ((Fun 𝐹 B dom 𝐹) → φ)
72, 5, 6syl2anc 393 1 ((𝐹 Fn A B A) → φ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1370  dom cdm 4268  Fun wfun 4819   Fn wfn 4820
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 1312  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-4 1377  ax-17 1396  ax-ial 1405  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-cleq 2011  df-clel 2014  df-fn 4828
This theorem is referenced by:  fneu  4925  fnbrfvb  5135  fvelrnb  5142  fvelimab  5150  fniinfv  5152  fvco2  5163  eqfnfv  5186  fndmdif  5193  fndmin  5195  elpreima  5207  fniniseg  5208  fniniseg2  5210  fnniniseg2  5211  rexsupp  5212  fnopfv  5218  fnfvelrn  5220  rexrn  5225  ralrn  5226  fsn2  5258  fnressn  5270  eufnfv  5310  rexima  5315  ralima  5316  fniunfv  5322  dff13  5328  foeqcnvco  5351  f1eqcocnv  5352  isocnv2  5373  isoini  5378  f1oiso  5386  fnovex  5458  suppssof1  5647  offveqb  5649  1stexg  5713  2ndexg  5714  smoiso  5835  rdgruledefgg  5878  rdgi0g  5882  rdgivallem  5884  rdg0  5891  frecabex  5895  frectfr  5896
  Copyright terms: Public domain W3C validator