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

Theorem funfni 4999
 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 4996 . . 3 (𝐹 Fn 𝐴 → Fun 𝐹)
21adantr 261 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → Fun 𝐹)
3 fndm 4998 . . . 4 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
43eleq2d 2107 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹𝐵𝐴))
54biimpar 281 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → 𝐵 ∈ dom 𝐹)
6 funfni.1 . 2 ((Fun 𝐹𝐵 ∈ dom 𝐹) → 𝜑)
72, 5, 6syl2anc 391 1 ((𝐹 Fn 𝐴𝐵𝐴) → 𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∈ wcel 1393  dom cdm 4345  Fun wfun 4896   Fn wfn 4897 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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036  df-fn 4905 This theorem is referenced by:  fneu  5003  fnbrfvb  5214  fvelrnb  5221  fvelimab  5229  fniinfv  5231  fvco2  5242  eqfnfv  5265  fndmdif  5272  fndmin  5274  elpreima  5286  fniniseg  5287  fniniseg2  5289  fnniniseg2  5290  rexsupp  5291  fnopfv  5297  fnfvelrn  5299  rexrn  5304  ralrn  5305  fsn2  5337  fnressn  5349  eufnfv  5389  rexima  5394  ralima  5395  fniunfv  5401  dff13  5407  foeqcnvco  5430  f1eqcocnv  5431  isocnv2  5452  isoini  5457  f1oiso  5465  fnovex  5538  suppssof1  5728  offveqb  5730  1stexg  5794  2ndexg  5795  smoiso  5917  rdgruledefgg  5962  rdgivallem  5968  frectfr  5985  frecrdg  5992  freccl  5993  en1  6279  ordiso2  6357
 Copyright terms: Public domain W3C validator