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

Theorem funfni 5067
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 5064 . . 3 (𝐹 Fn 𝐴 → Fun 𝐹)
21adantr 270 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → Fun 𝐹)
3 fndm 5066 . . . 4 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
43eleq2d 2152 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹𝐵𝐴))
54biimpar 291 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → 𝐵 ∈ dom 𝐹)
6 funfni.1 . 2 ((Fun 𝐹𝐵 ∈ dom 𝐹) → 𝜑)
72, 5, 6syl2anc 403 1 ((𝐹 Fn 𝐴𝐵𝐴) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1434  dom cdm 4401  Fun wfun 4963   Fn wfn 4964
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-clel 2079  df-fn 4972
This theorem is referenced by:  fneu  5071  fnbrfvb  5290  fvelrnb  5297  fvelimab  5305  fniinfv  5307  fvco2  5318  eqfnfv  5342  fndmdif  5349  fndmin  5351  elpreima  5363  fniniseg  5364  fniniseg2  5366  fnniniseg2  5367  rexsupp  5368  fnopfv  5374  fnfvelrn  5376  rexrn  5381  ralrn  5382  fsn2  5413  fnressn  5425  eufnfv  5465  rexima  5474  ralima  5475  fniunfv  5481  dff13  5487  foeqcnvco  5509  f1eqcocnv  5510  isocnv2  5531  isoini  5536  f1oiso  5544  fnovex  5617  suppssof1  5807  offveqb  5809  1stexg  5873  2ndexg  5874  smoiso  5999  rdgruledefgg  6072  rdgivallem  6078  frectfr  6097  frecrdg  6105  en1  6446  fnfi  6571  ordiso2  6635
  Copyright terms: Public domain W3C validator