Theorem funfni 5457

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 5452	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 276	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5454	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2302	. . 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 2203  dom cdm 4748  Fun wfun 5345   Fn wfn 5346

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228  df-fn 5354

This theorem is referenced by:  fneu  5461  fnbrfvb  5714  fvelrnb  5723  fvelimab  5732  fniinfv  5734  fvco2  5745  eqfnfv  5774  fndmdif  5782  fndmin  5784  elpreima  5796  fniniseg  5797  fniniseg2  5799  fnniniseg2  5800  fnopfv  5806  fnfvelrn  5808  rexrn  5813  ralrn  5814  fsn2  5850  fnressn  5869  eufnfv  5916  rexima  5926  ralima  5927  fniunfv  5934  dff13  5940  foeqcnvco  5962  f1eqcocnv  5963  isocnv2  5984  isoini  5990  f1oiso  5998  fnovex  6082  suppssof1  6283  offveqb  6285  1stexg  6360  2ndexg  6361  smoiso  6532  rdgruledefgg  6605  rdgivallem  6611  frectfr  6630  frecrdg  6638  en1  7038  fnfi  7202  ordiso2  7325  cc2lem  7579  slotex  13231  ressbas2d  13273  ressbasid  13275  strressid  13276  ressval3d  13277  prdsex  13474  prdsval  13478  prdsbaslemss  13479  prdsbas  13481  prdsplusg  13482  prdsmulr  13483  pwsbas  13497  pwselbasb  13498  pwssnf1o  13503  imasex  13510  imasival  13511  imasbas  13512  imasplusg  13513  imasmulr  13514  imasaddfn  13522  imasaddval  13523  imasaddf  13524  imasmulfn  13525  imasmulval  13526  imasmulf  13527  qusval  13528  qusex  13530  qusaddvallemg  13538  qusaddflemg  13539  qusaddval  13540  qusaddf  13541  qusmulval  13542  qusmulf  13543  xpsfeq  13550  xpsval  13557  ismgm  13562  plusffvalg  13567  grpidvalg  13578  fn0g  13580  fngsum  13593  igsumvalx  13594  gsumfzval  13596  gsumress  13600  gsum0g  13601  issgrp  13608  ismnddef  13623  issubmnd  13647  ress0g  13648  ismhm  13666  mhmex  13667  issubm  13677  0mhm  13691  grppropstrg  13724  grpinvfvalg  13747  grpinvval  13748  grpinvfng  13749  grpsubfvalg  13750  grpsubval  13751  grpressid  13766  grplactfval  13806  qusgrp2  13822  mulgfvalg  13830  mulgval  13831  mulgex  13832  mulgfng  13833  issubg  13882  subgex  13885  issubg2m  13898  isnsg  13911  releqgg  13929  eqgex  13930  eqgfval  13931  eqgen  13936  isghm  13952  ablressid  14044  mgptopng  14065  isrng  14070  rngressid  14090  qusrng  14094  dfur2g  14098  issrg  14101  isring  14136  ringidss  14165  ringressid  14199  qusring2  14202  dvdsrvald  14230  dvdsrex  14235  unitgrp  14253  unitabl  14254  invrfvald  14259  unitlinv  14263  unitrinv  14264  dvrfvald  14270  rdivmuldivd  14281  invrpropdg  14286  dfrhm2  14291  rhmex  14294  rhmunitinv  14315  isnzr2  14321  issubrng  14336  issubrg  14358  subrgugrp  14377  rrgval  14399  isdomn  14407  aprval  14420  aprap  14424  islmod  14431  scaffvalg  14446  rmodislmod  14491  lssex  14494  lsssetm  14496  islssm  14497  islssmg  14498  islss3  14519  lspfval  14528  lspval  14530  lspcl  14531  lspex  14535  sraval  14577  sralemg  14578  srascag  14582  sravscag  14583  sraipg  14584  sraex  14586  rlmsubg  14598  rlmvnegg  14605  ixpsnbasval  14606  lidlex  14613  rspex  14614  lidlss  14616  lidlrsppropdg  14635  qusrhm  14668  mopnset  14692  psrval  14806  fnpsr  14807  psrbasg  14821  psrelbas  14822  psrplusgg  14825  psraddcl  14827  psr0cl  14828  psrnegcl  14830  psr1clfi  14835  mplvalcoe  14837  fnmpl  14840  mplplusgg  14850  vtxvalg  16003  vtxex  16005