Theorem funfni 5382

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

Step	Hyp	Ref	Expression
1		fnfun 5377	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 276	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5379	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2276	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	4	biimpar 297	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ dom 𝐹)
6		funfni.1	. 2 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑)
7	2, 5, 6	syl2anc 411	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  dom cdm 4680  Fun wfun 5271   Fn wfn 5272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202  df-fn 5280

This theorem is referenced by:  fneu  5386  fnbrfvb  5629  fvelrnb  5636  fvelimab  5645  fniinfv  5647  fvco2  5658  eqfnfv  5687  fndmdif  5695  fndmin  5697  elpreima  5709  fniniseg  5710  fniniseg2  5712  fnniniseg2  5713  rexsupp  5714  fnopfv  5720  fnfvelrn  5722  rexrn  5727  ralrn  5728  fsn2  5764  fnressn  5780  eufnfv  5825  rexima  5833  ralima  5834  fniunfv  5841  dff13  5847  foeqcnvco  5869  f1eqcocnv  5870  isocnv2  5891  isoini  5897  f1oiso  5905  fnovex  5987  suppssof1  6186  offveqb  6188  1stexg  6263  2ndexg  6264  smoiso  6398  rdgruledefgg  6471  rdgivallem  6477  frectfr  6496  frecrdg  6504  en1  6901  fnfi  7050  ordiso2  7149  cc2lem  7391  slotex  12909  ressbas2d  12950  ressbasid  12952  strressid  12953  ressval3d  12954  prdsex  13151  prdsval  13155  prdsbaslemss  13156  prdsbas  13158  prdsplusg  13159  prdsmulr  13160  pwsbas  13174  pwselbasb  13175  pwssnf1o  13180  imasex  13187  imasival  13188  imasbas  13189  imasplusg  13190  imasmulr  13191  imasaddfn  13199  imasaddval  13200  imasaddf  13201  imasmulfn  13202  imasmulval  13203  imasmulf  13204  qusval  13205  qusex  13207  qusaddvallemg  13215  qusaddflemg  13216  qusaddval  13217  qusaddf  13218  qusmulval  13219  qusmulf  13220  xpsfeq  13227  xpsval  13234  ismgm  13239  plusffvalg  13244  grpidvalg  13255  fn0g  13257  fngsum  13270  igsumvalx  13271  gsumfzval  13273  gsumress  13277  gsum0g  13278  issgrp  13285  ismnddef  13300  issubmnd  13324  ress0g  13325  ismhm  13343  mhmex  13344  issubm  13354  0mhm  13368  grppropstrg  13401  grpinvfvalg  13424  grpinvval  13425  grpinvfng  13426  grpsubfvalg  13427  grpsubval  13428  grpressid  13443  grplactfval  13483  qusgrp2  13499  mulgfvalg  13507  mulgval  13508  mulgex  13509  mulgfng  13510  issubg  13559  subgex  13562  issubg2m  13575  isnsg  13588  releqgg  13606  eqgex  13607  eqgfval  13608  eqgen  13613  isghm  13629  ablressid  13721  mgptopng  13741  isrng  13746  rngressid  13766  qusrng  13770  dfur2g  13774  issrg  13777  isring  13812  ringidss  13841  ringressid  13875  qusring2  13878  reldvdsrsrg  13904  dvdsrvald  13905  dvdsrex  13910  unitgrp  13928  unitabl  13929  invrfvald  13934  unitlinv  13938  unitrinv  13939  dvrfvald  13945  rdivmuldivd  13956  invrpropdg  13961  dfrhm2  13966  rhmex  13969  rhmunitinv  13990  isnzr2  13996  issubrng  14011  issubrg  14033  subrgugrp  14052  rrgval  14074  isdomn  14081  aprval  14094  aprap  14098  islmod  14103  scaffvalg  14118  rmodislmod  14163  lssex  14166  lsssetm  14168  islssm  14169  islssmg  14170  islss3  14191  lspfval  14200  lspval  14202  lspcl  14203  lspex  14207  sraval  14249  sralemg  14250  srascag  14254  sravscag  14255  sraipg  14256  sraex  14258  rlmsubg  14270  rlmvnegg  14277  ixpsnbasval  14278  lidlex  14285  rspex  14286  lidlss  14288  lidlrsppropdg  14307  qusrhm  14340  mopnset  14364  psrval  14478  fnpsr  14479  psrbasg  14486  psrelbas  14487  psrplusgg  14490  psraddcl  14492  psr0cl  14493  psrnegcl  14495  psr1clfi  14500  mplvalcoe  14502  fnmpl  14505  mplplusgg  14515  vtxvalg  15665  vtxex  15667