Theorem funfni 5432

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 5427	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 276	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5429	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2301	. . 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 2202  dom cdm 4725  Fun wfun 5320   Fn wfn 5321

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-fn 5329

This theorem is referenced by:  fneu  5436  fnbrfvb  5684  fvelrnb  5693  fvelimab  5702  fniinfv  5704  fvco2  5715  eqfnfv  5744  fndmdif  5752  fndmin  5754  elpreima  5766  fniniseg  5767  fniniseg2  5769  fnniniseg2  5770  rexsupp  5771  fnopfv  5777  fnfvelrn  5779  rexrn  5784  ralrn  5785  fsn2  5821  fnressn  5840  eufnfv  5885  rexima  5895  ralima  5896  fniunfv  5903  dff13  5909  foeqcnvco  5931  f1eqcocnv  5932  isocnv2  5953  isoini  5959  f1oiso  5967  fnovex  6051  suppssof1  6253  offveqb  6255  1stexg  6330  2ndexg  6331  smoiso  6468  rdgruledefgg  6541  rdgivallem  6547  frectfr  6566  frecrdg  6574  en1  6973  fnfi  7135  ordiso2  7234  cc2lem  7485  slotex  13114  ressbas2d  13156  ressbasid  13158  strressid  13159  ressval3d  13160  prdsex  13357  prdsval  13361  prdsbaslemss  13362  prdsbas  13364  prdsplusg  13365  prdsmulr  13366  pwsbas  13380  pwselbasb  13381  pwssnf1o  13386  imasex  13393  imasival  13394  imasbas  13395  imasplusg  13396  imasmulr  13397  imasaddfn  13405  imasaddval  13406  imasaddf  13407  imasmulfn  13408  imasmulval  13409  imasmulf  13410  qusval  13411  qusex  13413  qusaddvallemg  13421  qusaddflemg  13422  qusaddval  13423  qusaddf  13424  qusmulval  13425  qusmulf  13426  xpsfeq  13433  xpsval  13440  ismgm  13445  plusffvalg  13450  grpidvalg  13461  fn0g  13463  fngsum  13476  igsumvalx  13477  gsumfzval  13479  gsumress  13483  gsum0g  13484  issgrp  13491  ismnddef  13506  issubmnd  13530  ress0g  13531  ismhm  13549  mhmex  13550  issubm  13560  0mhm  13574  grppropstrg  13607  grpinvfvalg  13630  grpinvval  13631  grpinvfng  13632  grpsubfvalg  13633  grpsubval  13634  grpressid  13649  grplactfval  13689  qusgrp2  13705  mulgfvalg  13713  mulgval  13714  mulgex  13715  mulgfng  13716  issubg  13765  subgex  13768  issubg2m  13781  isnsg  13794  releqgg  13812  eqgex  13813  eqgfval  13814  eqgen  13819  isghm  13835  ablressid  13927  mgptopng  13948  isrng  13953  rngressid  13973  qusrng  13977  dfur2g  13981  issrg  13984  isring  14019  ringidss  14048  ringressid  14082  qusring2  14085  dvdsrvald  14113  dvdsrex  14118  unitgrp  14136  unitabl  14137  invrfvald  14142  unitlinv  14146  unitrinv  14147  dvrfvald  14153  rdivmuldivd  14164  invrpropdg  14169  dfrhm2  14174  rhmex  14177  rhmunitinv  14198  isnzr2  14204  issubrng  14219  issubrg  14241  subrgugrp  14260  rrgval  14282  isdomn  14289  aprval  14302  aprap  14306  islmod  14311  scaffvalg  14326  rmodislmod  14371  lssex  14374  lsssetm  14376  islssm  14377  islssmg  14378  islss3  14399  lspfval  14408  lspval  14410  lspcl  14411  lspex  14415  sraval  14457  sralemg  14458  srascag  14462  sravscag  14463  sraipg  14464  sraex  14466  rlmsubg  14478  rlmvnegg  14485  ixpsnbasval  14486  lidlex  14493  rspex  14494  lidlss  14496  lidlrsppropdg  14515  qusrhm  14548  mopnset  14572  psrval  14686  fnpsr  14687  psrbasg  14694  psrelbas  14695  psrplusgg  14698  psraddcl  14700  psr0cl  14701  psrnegcl  14703  psr1clfi  14708  mplvalcoe  14710  fnmpl  14713  mplplusgg  14723  vtxvalg  15873  vtxex  15875