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

Theorem funfni 5026
Description: Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.)
Hypothesis
Ref Expression
funfni.1 ((Fun 𝐹𝐵 ∈ dom 𝐹) → 𝜑)
Assertion
Ref Expression
funfni ((𝐹 Fn 𝐴𝐵𝐴) → 𝜑)

Proof of Theorem funfni
StepHypRef Expression
1 fnfun 5023 . . 3 (𝐹 Fn 𝐴 → Fun 𝐹)
21adantr 265 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → Fun 𝐹)
3 fndm 5025 . . . 4 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
43eleq2d 2123 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹𝐵𝐴))
54biimpar 285 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → 𝐵 ∈ dom 𝐹)
6 funfni.1 . 2 ((Fun 𝐹𝐵 ∈ dom 𝐹) → 𝜑)
72, 5, 6syl2anc 397 1 ((𝐹 Fn 𝐴𝐵𝐴) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wcel 1409  dom cdm 4372  Fun wfun 4923   Fn wfn 4924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052  df-fn 4932
This theorem is referenced by:  fneu  5030  fnbrfvb  5241  fvelrnb  5248  fvelimab  5256  fniinfv  5258  fvco2  5269  eqfnfv  5292  fndmdif  5299  fndmin  5301  elpreima  5313  fniniseg  5314  fniniseg2  5316  fnniniseg2  5317  rexsupp  5318  fnopfv  5324  fnfvelrn  5326  rexrn  5331  ralrn  5332  fsn2  5364  fnressn  5376  eufnfv  5416  rexima  5421  ralima  5422  fniunfv  5428  dff13  5434  foeqcnvco  5457  f1eqcocnv  5458  isocnv2  5479  isoini  5484  f1oiso  5492  fnovex  5565  suppssof1  5755  offveqb  5757  1stexg  5821  2ndexg  5822  smoiso  5947  rdgruledefgg  5992  rdgivallem  5998  frectfr  6015  frecrdg  6022  freccl  6023  en1  6309  ordiso2  6414
  Copyright terms: Public domain W3C validator