Theorem funfni 5359

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 5356	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 276	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5358	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2266	. . 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 2167  dom cdm 4664  Fun wfun 5253   Fn wfn 5254

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192  df-fn 5262

This theorem is referenced by:  fneu  5363  fnbrfvb  5602  fvelrnb  5609  fvelimab  5618  fniinfv  5620  fvco2  5631  eqfnfv  5660  fndmdif  5668  fndmin  5670  elpreima  5682  fniniseg  5683  fniniseg2  5685  fnniniseg2  5686  rexsupp  5687  fnopfv  5693  fnfvelrn  5695  rexrn  5700  ralrn  5701  fsn2  5737  fnressn  5749  eufnfv  5794  rexima  5802  ralima  5803  fniunfv  5810  dff13  5816  foeqcnvco  5838  f1eqcocnv  5839  isocnv2  5860  isoini  5866  f1oiso  5874  fnovex  5956  suppssof1  6155  offveqb  6157  1stexg  6227  2ndexg  6228  smoiso  6362  rdgruledefgg  6435  rdgivallem  6441  frectfr  6460  frecrdg  6468  en1  6860  fnfi  7004  ordiso2  7103  cc2lem  7336  slotex  12716  ressbas2d  12757  ressbasid  12759  strressid  12760  ressval3d  12761  prdsex  12957  prdsval  12961  prdsbaslemss  12962  prdsbas  12964  prdsplusg  12965  prdsmulr  12966  imasex  12974  imasival  12975  imasbas  12976  imasplusg  12977  imasmulr  12978  imasaddfn  12986  imasaddval  12987  imasaddf  12988  imasmulfn  12989  imasmulval  12990  imasmulf  12991  qusval  12992  qusex  12994  qusaddvallemg  13002  qusaddflemg  13003  qusaddval  13004  qusaddf  13005  qusmulval  13006  qusmulf  13007  xpsfeq  13014  xpsval  13021  ismgm  13026  plusffvalg  13031  grpidvalg  13042  fn0g  13044  fngsum  13057  igsumvalx  13058  gsumfzval  13060  gsumress  13064  gsum0g  13065  issgrp  13072  ismnddef  13085  issubmnd  13109  ress0g  13110  ismhm  13119  mhmex  13120  issubm  13130  0mhm  13144  grppropstrg  13177  grpinvfvalg  13200  grpinvval  13201  grpinvfng  13202  grpsubfvalg  13203  grpsubval  13204  grpressid  13219  grplactfval  13259  qusgrp2  13269  mulgfvalg  13277  mulgval  13278  mulgex  13279  mulgfng  13280  issubg  13329  subgex  13332  issubg2m  13345  isnsg  13358  releqgg  13376  eqgex  13377  eqgfval  13378  eqgen  13383  isghm  13399  ablressid  13491  mgptopng  13511  isrng  13516  rngressid  13536  qusrng  13540  dfur2g  13544  issrg  13547  isring  13582  ringidss  13611  ringressid  13645  qusring2  13648  reldvdsrsrg  13674  dvdsrvald  13675  dvdsrex  13680  unitgrp  13698  unitabl  13699  invrfvald  13704  unitlinv  13708  unitrinv  13709  dvrfvald  13715  rdivmuldivd  13726  invrpropdg  13731  dfrhm2  13736  rhmex  13739  rhmunitinv  13760  isnzr2  13766  issubrng  13781  issubrg  13803  subrgugrp  13822  rrgval  13844  isdomn  13851  aprval  13864  aprap  13868  islmod  13873  scaffvalg  13888  rmodislmod  13933  lssex  13936  lsssetm  13938  islssm  13939  islssmg  13940  islss3  13961  lspfval  13970  lspval  13972  lspcl  13973  lspex  13977  sraval  14019  sralemg  14020  srascag  14024  sravscag  14025  sraipg  14026  sraex  14028  rlmsubg  14040  rlmvnegg  14047  ixpsnbasval  14048  lidlex  14055  rspex  14056  lidlss  14058  lidlrsppropdg  14077  qusrhm  14110  mopnset  14134  psrval  14246  fnpsr  14247  psrbasg  14253  psrelbas  14254  psrplusgg  14256  psraddcl  14258