Theorem funfni 5463

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 5458	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 276	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5460	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2304	. . 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 2205  dom cdm 4754  Fun wfun 5351   Fn wfn 5352

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 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230  df-fn 5360

This theorem is referenced by:  fneu  5467  fnbrfvb  5720  fvelrnb  5729  fvelimab  5738  fniinfv  5740  fvco2  5751  eqfnfv  5780  fndmdif  5788  fndmin  5790  elpreima  5802  fniniseg  5803  fniniseg2  5805  fnniniseg2  5806  fnopfv  5812  fnfvelrn  5814  rexrn  5819  ralrn  5820  fsn2  5856  fnressn  5875  eufnfv  5922  rexima  5933  ralima  5934  fniunfv  5941  dff13  5947  foeqcnvco  5969  f1eqcocnv  5970  isocnv2  5991  isoini  5997  f1oiso  6005  fnovex  6091  suppssof1  6293  offveqb  6295  1stexg  6374  2ndexg  6375  smoiso  6546  rdgruledefgg  6619  rdgivallem  6625  frectfr  6644  frecrdg  6652  en1  7052  fnfi  7216  ordiso2  7339  cc2lem  7596  slotex  13323  ressbas2d  13365  ressbasid  13367  strressid  13368  ressval3d  13369  prdsex  13566  prdsval  13570  prdsbaslemss  13571  prdsbas  13573  prdsplusg  13574  prdsmulr  13575  pwsbas  13589  pwselbasb  13590  pwssnf1o  13595  imasex  13602  imasival  13603  imasbas  13604  imasplusg  13605  imasmulr  13606  imasaddfn  13614  imasaddval  13615  imasaddf  13616  imasmulfn  13617  imasmulval  13618  imasmulf  13619  qusval  13620  qusex  13622  qusaddvallemg  13630  qusaddflemg  13631  qusaddval  13632  qusaddf  13633  qusmulval  13634  qusmulf  13635  xpsfeq  13642  xpsval  13649  ismgm  13654  plusffvalg  13659  grpidvalg  13670  fn0g  13672  fngsum  13685  igsumvalx  13686  gsumfzval  13688  gsumress  13692  gsum0g  13693  issgrp  13700  ismnddef  13715  issubmnd  13739  ress0g  13740  ismhm  13758  mhmex  13759  issubm  13769  0mhm  13783  grppropstrg  13816  grpinvfvalg  13839  grpinvval  13840  grpinvfng  13841  grpsubfvalg  13842  grpsubval  13843  grpressid  13858  grplactfval  13898  qusgrp2  13914  mulgfvalg  13922  mulgval  13923  mulgex  13924  mulgfng  13925  issubg  13974  subgex  13977  issubg2m  13990  isnsg  14003  releqgg  14021  eqgex  14022  eqgfval  14023  eqgen  14028  isghm  14044  ablressid  14136  mgptopng  14157  isrng  14162  rngressid  14182  qusrng  14186  dfur2g  14190  issrg  14193  isring  14228  ringidss  14257  ringressid  14291  qusring2  14294  dvdsrvald  14323  dvdsrex  14328  unitgrp  14346  unitabl  14347  invrfvald  14352  unitlinv  14356  unitrinv  14357  dvrfvald  14363  rdivmuldivd  14374  invrpropdg  14379  dfrhm2  14384  rhmex  14387  rhmunitinv  14408  isnzr2  14414  issubrng  14430  issubrg  14452  subrgugrp  14471  rrgval  14493  isdomn  14501  aprval  14514  aprap  14521  aprprop  14524  islmod  14551  scaffvalg  14566  rmodislmod  14611  lssex  14614  lsssetm  14616  islssm  14617  islssmg  14618  islss3  14639  lspfval  14648  lspval  14650  lspcl  14651  lspex  14655  sraval  14697  sralemg  14698  srascag  14702  sravscag  14703  sraipg  14704  sraex  14706  rlmsubg  14718  rlmvnegg  14725  ixpsnbasval  14726  lidlex  14733  rspex  14734  lidlss  14736  lidlrsppropdg  14755  qusrhm  14788  mopnset  14812  psrval  14926  fnpsr  14927  psrbasg  14941  psrelbas  14942  psrplusgg  14945  psraddcl  14947  psr0cl  14948  psrnegcl  14950  psr1clfi  14955  mplvalcoe  14957  fnmpl  14960  mplplusgg  14970  vtxvalg  16123  vtxex  16125