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

Theorem funfni 5114
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 5111 . . 3 (𝐹 Fn 𝐴 → Fun 𝐹)
21adantr 270 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → Fun 𝐹)
3 fndm 5113 . . . 4 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
43eleq2d 2157 . . 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 1438  dom cdm 4438  Fun wfun 5009   Fn wfn 5010
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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084  df-fn 5018
This theorem is referenced by:  fneu  5118  fnbrfvb  5345  fvelrnb  5352  fvelimab  5360  fniinfv  5362  fvco2  5373  eqfnfv  5397  fndmdif  5404  fndmin  5406  elpreima  5418  fniniseg  5419  fniniseg2  5421  fnniniseg2  5422  rexsupp  5423  fnopfv  5429  fnfvelrn  5431  rexrn  5436  ralrn  5437  fsn2  5471  fnressn  5483  eufnfv  5525  rexima  5534  ralima  5535  fniunfv  5541  dff13  5547  foeqcnvco  5569  f1eqcocnv  5570  isocnv2  5591  isoini  5597  f1oiso  5605  fnovex  5682  suppssof1  5872  offveqb  5874  1stexg  5938  2ndexg  5939  smoiso  6067  rdgruledefgg  6140  rdgivallem  6146  frectfr  6165  frecrdg  6173  en1  6516  fnfi  6646  ordiso2  6728
  Copyright terms: Public domain W3C validator