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

Theorem funfni 5298
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 5295 . . 3 (𝐹 Fn 𝐴 → Fun 𝐹)
21adantr 274 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → Fun 𝐹)
3 fndm 5297 . . . 4 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
43eleq2d 2240 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹𝐵𝐴))
54biimpar 295 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → 𝐵 ∈ dom 𝐹)
6 funfni.1 . 2 ((Fun 𝐹𝐵 ∈ dom 𝐹) → 𝜑)
72, 5, 6syl2anc 409 1 ((𝐹 Fn 𝐴𝐵𝐴) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 2141  dom cdm 4611  Fun wfun 5192   Fn wfn 5193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166  df-fn 5201
This theorem is referenced by:  fneu  5302  fnbrfvb  5537  fvelrnb  5544  fvelimab  5552  fniinfv  5554  fvco2  5565  eqfnfv  5593  fndmdif  5601  fndmin  5603  elpreima  5615  fniniseg  5616  fniniseg2  5618  fnniniseg2  5619  rexsupp  5620  fnopfv  5626  fnfvelrn  5628  rexrn  5633  ralrn  5634  fsn2  5670  fnressn  5682  eufnfv  5726  rexima  5734  ralima  5735  fniunfv  5741  dff13  5747  foeqcnvco  5769  f1eqcocnv  5770  isocnv2  5791  isoini  5797  f1oiso  5805  fnovex  5886  suppssof1  6078  offveqb  6080  1stexg  6146  2ndexg  6147  smoiso  6281  rdgruledefgg  6354  rdgivallem  6360  frectfr  6379  frecrdg  6387  en1  6777  fnfi  6914  ordiso2  7012  cc2lem  7228  slotex  12443  ismgm  12611  plusffvalg  12616  grpidvalg  12627  fn0g  12629  issgrp  12644  ismnddef  12654  ismhm  12685  issubm  12695  0mhm  12704  grpinvfvalg  12745  grpinvval  12746  grpinvfng  12747  grpsubfvalg  12748  grpsubval  12749
  Copyright terms: Public domain W3C validator