Theorem funfni 5419

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 5414	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 276	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5416	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2299	. . 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 2200  dom cdm 4716  Fun wfun 5308   Fn wfn 5309

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-fn 5317

This theorem is referenced by:  fneu  5423  fnbrfvb  5666  fvelrnb  5674  fvelimab  5683  fniinfv  5685  fvco2  5696  eqfnfv  5725  fndmdif  5733  fndmin  5735  elpreima  5747  fniniseg  5748  fniniseg2  5750  fnniniseg2  5751  rexsupp  5752  fnopfv  5758  fnfvelrn  5760  rexrn  5765  ralrn  5766  fsn2  5802  fnressn  5818  eufnfv  5863  rexima  5871  ralima  5872  fniunfv  5879  dff13  5885  foeqcnvco  5907  f1eqcocnv  5908  isocnv2  5929  isoini  5935  f1oiso  5943  fnovex  6027  suppssof1  6226  offveqb  6228  1stexg  6303  2ndexg  6304  smoiso  6438  rdgruledefgg  6511  rdgivallem  6517  frectfr  6536  frecrdg  6544  en1  6941  fnfi  7091  ordiso2  7190  cc2lem  7440  slotex  13045  ressbas2d  13087  ressbasid  13089  strressid  13090  ressval3d  13091  prdsex  13288  prdsval  13292  prdsbaslemss  13293  prdsbas  13295  prdsplusg  13296  prdsmulr  13297  pwsbas  13311  pwselbasb  13312  pwssnf1o  13317  imasex  13324  imasival  13325  imasbas  13326  imasplusg  13327  imasmulr  13328  imasaddfn  13336  imasaddval  13337  imasaddf  13338  imasmulfn  13339  imasmulval  13340  imasmulf  13341  qusval  13342  qusex  13344  qusaddvallemg  13352  qusaddflemg  13353  qusaddval  13354  qusaddf  13355  qusmulval  13356  qusmulf  13357  xpsfeq  13364  xpsval  13371  ismgm  13376  plusffvalg  13381  grpidvalg  13392  fn0g  13394  fngsum  13407  igsumvalx  13408  gsumfzval  13410  gsumress  13414  gsum0g  13415  issgrp  13422  ismnddef  13437  issubmnd  13461  ress0g  13462  ismhm  13480  mhmex  13481  issubm  13491  0mhm  13505  grppropstrg  13538  grpinvfvalg  13561  grpinvval  13562  grpinvfng  13563  grpsubfvalg  13564  grpsubval  13565  grpressid  13580  grplactfval  13620  qusgrp2  13636  mulgfvalg  13644  mulgval  13645  mulgex  13646  mulgfng  13647  issubg  13696  subgex  13699  issubg2m  13712  isnsg  13725  releqgg  13743  eqgex  13744  eqgfval  13745  eqgen  13750  isghm  13766  ablressid  13858  mgptopng  13878  isrng  13883  rngressid  13903  qusrng  13907  dfur2g  13911  issrg  13914  isring  13949  ringidss  13978  ringressid  14012  qusring2  14015  reldvdsrsrg  14041  dvdsrvald  14042  dvdsrex  14047  unitgrp  14065  unitabl  14066  invrfvald  14071  unitlinv  14075  unitrinv  14076  dvrfvald  14082  rdivmuldivd  14093  invrpropdg  14098  dfrhm2  14103  rhmex  14106  rhmunitinv  14127  isnzr2  14133  issubrng  14148  issubrg  14170  subrgugrp  14189  rrgval  14211  isdomn  14218  aprval  14231  aprap  14235  islmod  14240  scaffvalg  14255  rmodislmod  14300  lssex  14303  lsssetm  14305  islssm  14306  islssmg  14307  islss3  14328  lspfval  14337  lspval  14339  lspcl  14340  lspex  14344  sraval  14386  sralemg  14387  srascag  14391  sravscag  14392  sraipg  14393  sraex  14395  rlmsubg  14407  rlmvnegg  14414  ixpsnbasval  14415  lidlex  14422  rspex  14423  lidlss  14425  lidlrsppropdg  14444  qusrhm  14477  mopnset  14501  psrval  14615  fnpsr  14616  psrbasg  14623  psrelbas  14624  psrplusgg  14627  psraddcl  14629  psr0cl  14630  psrnegcl  14632  psr1clfi  14637  mplvalcoe  14639  fnmpl  14642  mplplusgg  14652  vtxvalg  15802  vtxex  15804