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

Theorem funfni 5100
Description: Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.)
Hypothesis
Ref Expression
funfni.1  |-  ( ( Fun  F  /\  B  e.  dom  F )  ->  ph )
Assertion
Ref Expression
funfni  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ph )

Proof of Theorem funfni
StepHypRef Expression
1 fnfun 5097 . . 3  |-  ( F  Fn  A  ->  Fun  F )
21adantr 270 . 2  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  Fun  F )
3 fndm 5099 . . . 4  |-  ( F  Fn  A  ->  dom  F  =  A )
43eleq2d 2157 . . 3  |-  ( F  Fn  A  ->  ( B  e.  dom  F  <->  B  e.  A ) )
54biimpar 291 . 2  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  B  e.  dom  F
)
6 funfni.1 . 2  |-  ( ( Fun  F  /\  B  e.  dom  F )  ->  ph )
72, 5, 6syl2anc 403 1  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    e. wcel 1438   dom cdm 4428   Fun wfun 4996    Fn wfn 4997
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 5005
This theorem is referenced by:  fneu  5104  fnbrfvb  5329  fvelrnb  5336  fvelimab  5344  fniinfv  5346  fvco2  5357  eqfnfv  5381  fndmdif  5388  fndmin  5390  elpreima  5402  fniniseg  5403  fniniseg2  5405  fnniniseg2  5406  rexsupp  5407  fnopfv  5413  fnfvelrn  5415  rexrn  5420  ralrn  5421  fsn2  5455  fnressn  5467  eufnfv  5507  rexima  5516  ralima  5517  fniunfv  5523  dff13  5529  foeqcnvco  5551  f1eqcocnv  5552  isocnv2  5573  isoini  5579  f1oiso  5587  fnovex  5664  suppssof1  5854  offveqb  5856  1stexg  5920  2ndexg  5921  smoiso  6049  rdgruledefgg  6122  rdgivallem  6128  frectfr  6147  frecrdg  6155  en1  6496  fnfi  6625  ordiso2  6707
  Copyright terms: Public domain W3C validator