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  13327  ressbas2d  13369  ressbasid  13371  strressid  13372  ressval3d  13373  imasex  13573  imasival  13574  imasbas  13575  imasplusg  13576  imasmulr  13577  imasaddfn  13585  imasaddval  13586  imasaddf  13587  imasmulfn  13588  imasmulval  13589  imasmulf  13590  qusval  13591  qusex  13593  qusaddvallemg  13601  qusaddflemg  13602  qusaddval  13603  qusaddf  13604  qusmulval  13605  qusmulf  13606  xpsfeq  13613  ismgm  13624  plusffvalg  13629  grpidvalg  13640  fn0g  13642  fngsum  13655  igsumvalx  13656  gsumfzval  13658  gsumress  13662  gsum0g  13663  issgrp  13670  ismnddef  13683  issubmnd  13707  ress0g  13708  ismhm  13720  mhmex  13721  issubm  13731  0mhm  13745  grppropstrg  13778  grpinvfvalg  13801  grpinvval  13802  grpinvfng  13803  grpsubfvalg  13804  grpsubval  13805  grpressid  13820  grplactfval  13860  qusgrp2  13870  mulgfvalg  13878  mulgval  13879  mulgex  13880  mulgfng  13881  issubg  13930  subgex  13933  issubg2m  13946  isnsg  13959  releqgg  13977  eqgex  13978  eqgfval  13979  eqgen  13984  isghm  14000  ablressid  14092  prdsex  14118  prdsval  14119  prdsbaslemss  14120  prdsbas  14122  prdsplusg  14123  prdsmulr  14124  xpsval  14147  pwsbas  14151  pwselbasb  14152  pwssnf1o  14157  mgptopng  14172  isrng  14177  rngressid  14197  qusrng  14201  dfur2g  14209  issrg  14212  isring  14247  ringidss  14276  ringressid  14310  qusring2  14313  dvdsrvald  14342  dvdsrex  14347  unitgrp  14365  unitabl  14366  invrfvald  14371  unitlinv  14375  unitrinv  14376  dvrfvald  14382  rdivmuldivd  14393  invrpropdg  14398  dfrhm2  14403  rhmex  14406  rhmunitinv  14427  isnzr2  14433  issubrng  14449  issubrg  14471  subrgugrp  14490  rrgval  14512  isdomn  14520  aprval  14533  aprap  14540  aprprop  14543  islmod  14569  scaffvalg  14584  rmodislmod  14629  lssex  14632  lsssetm  14634  islssm  14635  islssmg  14636  islss3  14657  lspfval  14666  lspval  14668  lspcl  14669  lspex  14673  sraval  14715  sralemg  14716  srascag  14720  sravscag  14721  sraipg  14722  sraex  14724  rlmsubg  14736  rlmvnegg  14743  ixpsnbasval  14744  lidlex  14751  rspex  14752  lidlss  14754  lidlrsppropdg  14773  qusrhm  14806  mopnset  14830  psrval  14944  fnpsr  14945  psrbasg  14959  psrelbas  14960  psrplusgg  14963  psraddcl  14965  psr0cl  14966  psrnegcl  14968  psr1clfi  14973  mplvalcoe  14975  fnmpl  14978  mplplusgg  14988  vtxvalg  16141  vtxex  16143