Theorem funfni 5486

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 5481	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 276	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5483	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2308	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	4	biimpar 297	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ dom 𝐹)
6		funfni.1	. 2 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑)
7	2, 5, 6	syl2anc 415	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  dom cdm 4776  Fun wfun 5374   Fn wfn 5375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234  df-fn 5383

This theorem is used by:  fneu  5490  fnbrfvb  5744  fvelrnb  5753  fvelimab  5762  fniinfv  5764  fvco2  5777  eqfnfv  5809  fndmdif  5817  fndmin  5819  elpreima  5831  fniniseg  5832  fniniseg2  5834  fnniniseg2  5835  fnopfv  5841  fnfvelrn  5843  rexrn  5848  ralrn  5849  fsn2  5885  fnressn  5904  eufnfv  5952  rexima  5963  ralima  5964  fniunfv  5971  dff13  5977  foeqcnvco  5999  f1eqcocnv  6000  isocnv2  6021  isoini  6027  f1oiso  6035  fnovex  6121  suppssof1  6324  offveqb  6326  1stexg  6405  2ndexg  6406  smoiso  6577  rdgruledefgg  6650  rdgivallem  6656  frectfr  6675  frecrdg  6683  en1  7091  fnfi  7255  ordiso2  7382  cc2lem  7639  slotex  13438  ressbas2d  13482  ressbasid  13484  strressid  13485  ressval3d  13486  imasex  13686  imasival  13687  imasbas  13688  imasplusg  13689  imasmulr  13690  imasaddfn  13698  imasaddval  13699  imasaddf  13700  imasmulfn  13701  imasmulval  13702  imasmulf  13703  qusval  13704  qusex  13706  qusaddvallemg  13714  qusaddflemg  13715  qusaddval  13716  qusaddf  13717  qusmulval  13718  qusmulf  13719  xpsfeq  13726  ismgm  13737  plusffvalg  13742  grpidvalg  13753  fn0g  13755  fngzsum  13768  gzsumvalx  13769  gzsumfzval  13771  gzsumress  13772  gzsum0  13773  issgrp  13778  ismnddef  13791  issubmnd  13815  ress0g  13816  ismhm  13828  mhmex  13829  issubm  13839  0mhm  13853  grppropstrg  13884  grpinvfvalg  13907  grpinvval  13908  grpinvfng  13909  grpsubfvalg  13910  grpsubval  13911  grpressid  13926  grplactfval  13966  qusgrp2  13976  mulgfvalg  13984  mulgval  13985  mulgex  13986  mulgfng  13987  issubg  14036  subgex  14039  issubg2m  14052  isnsg  14065  releqgg  14083  eqgex  14084  eqgfval  14085  eqgen  14090  isghm  14106  cntzex  14151  cntrval  14152  cntzfval  14153  cntzval  14154  ablressid  14230  prdsex  14280  prdsval  14281  prdsbaslemss  14282  prdsbas  14284  prdsplusg  14285  prdsmulr  14286  xpsval  14309  pwsbas  14313  pwselbasb  14314  pwssnf1o  14319  mgptopng  14336  isrng  14341  rngressid  14361  qusrng  14365  dfur2g  14374  issrg  14377  isring  14412  ringidss  14442  ringressid  14478  qusring2  14481  dvdsrvald  14510  dvdsrex  14515  unitgrp  14533  unitabl  14534  invrfvald  14539  unitlinv  14543  unitrinv  14544  dvrfvald  14550  rdivmuldivd  14561  invrpropdg  14566  dfrhm2  14571  rhmex  14574  rhmunitinv  14595  isnzr2  14601  issubrng  14617  issubrg  14639  subrgugrp  14658  rrgval  14680  isdomn  14688  aprval  14701  aprap  14708  aprprop  14711  islmod  14737  scaffvalg  14753  rmodislmod  14798  lssex  14801  lsssetm  14803  islssm  14804  islssmg  14805  islss3  14826  lspfval  14835  lspval  14837  lspcl  14838  lspex  14842  sraval  14884  sralemg  14885  srascag  14889  sravscag  14890  sraipg  14891  sraex  14893  rlmsubg  14905  rlmvnegg  14912  ixpsnbasval  14913  lidlex  14920  rspex  14921  lidlss  14923  lidlrsppropdg  14942  qusrhm  14975  mopnset  14999  aspval  15125  asclfval  15131  psrval  15162  fnpsr  15163  psrbasg  15183  psrelbas  15184  psrplusgg  15187  psraddcl  15189  psrmulrg  15191  psrmulclfilem  15194  psr0cl  15196  psrnegcl  15198  psr1clfi  15203  psrlidmfi  15204  mvrval2  15212  mvrffi  15214  mplvalcoe  15218  fnmpl  15221  mplplusgg  15231  vtxvalg  16474  vtxex  16476