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

Theorem funfni 5030
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 5027 . . 3  |-  ( F  Fn  A  ->  Fun  F )
21adantr 270 . 2  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  Fun  F )
3 fndm 5029 . . . 4  |-  ( F  Fn  A  ->  dom  F  =  A )
43eleq2d 2149 . . 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 1434   dom cdm 4371   Fun wfun 4926    Fn wfn 4927
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 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078  df-fn 4935
This theorem is referenced by:  fneu  5034  fnbrfvb  5246  fvelrnb  5253  fvelimab  5261  fniinfv  5263  fvco2  5274  eqfnfv  5297  fndmdif  5304  fndmin  5306  elpreima  5318  fniniseg  5319  fniniseg2  5321  fnniniseg2  5322  rexsupp  5323  fnopfv  5329  fnfvelrn  5331  rexrn  5336  ralrn  5337  fsn2  5369  fnressn  5381  eufnfv  5421  rexima  5426  ralima  5427  fniunfv  5433  dff13  5439  foeqcnvco  5461  f1eqcocnv  5462  isocnv2  5483  isoini  5488  f1oiso  5496  fnovex  5569  suppssof1  5759  offveqb  5761  1stexg  5825  2ndexg  5826  smoiso  5951  rdgruledefgg  6024  rdgivallem  6030  frectfr  6049  frecrdg  6057  en1  6346  fnfi  6446  ordiso2  6505
  Copyright terms: Public domain W3C validator