Theorem funfni 5439

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 5434	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 276	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5436	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2301	. . 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 2202  dom cdm 4731  Fun wfun 5327   Fn wfn 5328

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 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-fn 5336

This theorem is referenced by:  fneu  5443  fnbrfvb  5693  fvelrnb  5702  fvelimab  5711  fniinfv  5713  fvco2  5724  eqfnfv  5753  fndmdif  5761  fndmin  5763  elpreima  5775  fniniseg  5776  fniniseg2  5778  fnniniseg2  5779  fnopfv  5785  fnfvelrn  5787  rexrn  5792  ralrn  5793  fsn2  5829  fnressn  5848  eufnfv  5895  rexima  5905  ralima  5906  fniunfv  5913  dff13  5919  foeqcnvco  5941  f1eqcocnv  5942  isocnv2  5963  isoini  5969  f1oiso  5977  fnovex  6061  suppssof1  6262  offveqb  6264  1stexg  6339  2ndexg  6340  smoiso  6511  rdgruledefgg  6584  rdgivallem  6590  frectfr  6609  frecrdg  6617  en1  7016  fnfi  7178  ordiso2  7277  cc2lem  7528  slotex  13170  ressbas2d  13212  ressbasid  13214  strressid  13215  ressval3d  13216  prdsex  13413  prdsval  13417  prdsbaslemss  13418  prdsbas  13420  prdsplusg  13421  prdsmulr  13422  pwsbas  13436  pwselbasb  13437  pwssnf1o  13442  imasex  13449  imasival  13450  imasbas  13451  imasplusg  13452  imasmulr  13453  imasaddfn  13461  imasaddval  13462  imasaddf  13463  imasmulfn  13464  imasmulval  13465  imasmulf  13466  qusval  13467  qusex  13469  qusaddvallemg  13477  qusaddflemg  13478  qusaddval  13479  qusaddf  13480  qusmulval  13481  qusmulf  13482  xpsfeq  13489  xpsval  13496  ismgm  13501  plusffvalg  13506  grpidvalg  13517  fn0g  13519  fngsum  13532  igsumvalx  13533  gsumfzval  13535  gsumress  13539  gsum0g  13540  issgrp  13547  ismnddef  13562  issubmnd  13586  ress0g  13587  ismhm  13605  mhmex  13606  issubm  13616  0mhm  13630  grppropstrg  13663  grpinvfvalg  13686  grpinvval  13687  grpinvfng  13688  grpsubfvalg  13689  grpsubval  13690  grpressid  13705  grplactfval  13745  qusgrp2  13761  mulgfvalg  13769  mulgval  13770  mulgex  13771  mulgfng  13772  issubg  13821  subgex  13824  issubg2m  13837  isnsg  13850  releqgg  13868  eqgex  13869  eqgfval  13870  eqgen  13875  isghm  13891  ablressid  13983  mgptopng  14004  isrng  14009  rngressid  14029  qusrng  14033  dfur2g  14037  issrg  14040  isring  14075  ringidss  14104  ringressid  14138  qusring2  14141  dvdsrvald  14169  dvdsrex  14174  unitgrp  14192  unitabl  14193  invrfvald  14198  unitlinv  14202  unitrinv  14203  dvrfvald  14209  rdivmuldivd  14220  invrpropdg  14225  dfrhm2  14230  rhmex  14233  rhmunitinv  14254  isnzr2  14260  issubrng  14275  issubrg  14297  subrgugrp  14316  rrgval  14338  isdomn  14345  aprval  14358  aprap  14362  islmod  14367  scaffvalg  14382  rmodislmod  14427  lssex  14430  lsssetm  14432  islssm  14433  islssmg  14434  islss3  14455  lspfval  14464  lspval  14466  lspcl  14467  lspex  14471  sraval  14513  sralemg  14514  srascag  14518  sravscag  14519  sraipg  14520  sraex  14522  rlmsubg  14534  rlmvnegg  14541  ixpsnbasval  14542  lidlex  14549  rspex  14550  lidlss  14552  lidlrsppropdg  14571  qusrhm  14604  mopnset  14628  psrval  14742  fnpsr  14743  psrbasg  14755  psrelbas  14756  psrplusgg  14759  psraddcl  14761  psr0cl  14762  psrnegcl  14764  psr1clfi  14769  mplvalcoe  14771  fnmpl  14774  mplplusgg  14784  vtxvalg  15937  vtxex  15939