Theorem funfni 5426

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 5421	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 276	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5423	. . . 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 4720  Fun wfun 5315   Fn wfn 5316

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 5324

This theorem is referenced by:  fneu  5430  fnbrfvb  5677  fvelrnb  5686  fvelimab  5695  fniinfv  5697  fvco2  5708  eqfnfv  5737  fndmdif  5745  fndmin  5747  elpreima  5759  fniniseg  5760  fniniseg2  5762  fnniniseg2  5763  rexsupp  5764  fnopfv  5770  fnfvelrn  5772  rexrn  5777  ralrn  5778  fsn2  5814  fnressn  5832  eufnfv  5877  rexima  5887  ralima  5888  fniunfv  5895  dff13  5901  foeqcnvco  5923  f1eqcocnv  5924  isocnv2  5945  isoini  5951  f1oiso  5959  fnovex  6043  suppssof1  6245  offveqb  6247  1stexg  6322  2ndexg  6323  smoiso  6459  rdgruledefgg  6532  rdgivallem  6538  frectfr  6557  frecrdg  6565  en1  6964  fnfi  7119  ordiso2  7218  cc2lem  7468  slotex  13080  ressbas2d  13122  ressbasid  13124  strressid  13125  ressval3d  13126  prdsex  13323  prdsval  13327  prdsbaslemss  13328  prdsbas  13330  prdsplusg  13331  prdsmulr  13332  pwsbas  13346  pwselbasb  13347  pwssnf1o  13352  imasex  13359  imasival  13360  imasbas  13361  imasplusg  13362  imasmulr  13363  imasaddfn  13371  imasaddval  13372  imasaddf  13373  imasmulfn  13374  imasmulval  13375  imasmulf  13376  qusval  13377  qusex  13379  qusaddvallemg  13387  qusaddflemg  13388  qusaddval  13389  qusaddf  13390  qusmulval  13391  qusmulf  13392  xpsfeq  13399  xpsval  13406  ismgm  13411  plusffvalg  13416  grpidvalg  13427  fn0g  13429  fngsum  13442  igsumvalx  13443  gsumfzval  13445  gsumress  13449  gsum0g  13450  issgrp  13457  ismnddef  13472  issubmnd  13496  ress0g  13497  ismhm  13515  mhmex  13516  issubm  13526  0mhm  13540  grppropstrg  13573  grpinvfvalg  13596  grpinvval  13597  grpinvfng  13598  grpsubfvalg  13599  grpsubval  13600  grpressid  13615  grplactfval  13655  qusgrp2  13671  mulgfvalg  13679  mulgval  13680  mulgex  13681  mulgfng  13682  issubg  13731  subgex  13734  issubg2m  13747  isnsg  13760  releqgg  13778  eqgex  13779  eqgfval  13780  eqgen  13785  isghm  13801  ablressid  13893  mgptopng  13913  isrng  13918  rngressid  13938  qusrng  13942  dfur2g  13946  issrg  13949  isring  13984  ringidss  14013  ringressid  14047  qusring2  14050  dvdsrvald  14078  dvdsrex  14083  unitgrp  14101  unitabl  14102  invrfvald  14107  unitlinv  14111  unitrinv  14112  dvrfvald  14118  rdivmuldivd  14129  invrpropdg  14134  dfrhm2  14139  rhmex  14142  rhmunitinv  14163  isnzr2  14169  issubrng  14184  issubrg  14206  subrgugrp  14225  rrgval  14247  isdomn  14254  aprval  14267  aprap  14271  islmod  14276  scaffvalg  14291  rmodislmod  14336  lssex  14339  lsssetm  14341  islssm  14342  islssmg  14343  islss3  14364  lspfval  14373  lspval  14375  lspcl  14376  lspex  14380  sraval  14422  sralemg  14423  srascag  14427  sravscag  14428  sraipg  14429  sraex  14431  rlmsubg  14443  rlmvnegg  14450  ixpsnbasval  14451  lidlex  14458  rspex  14459  lidlss  14461  lidlrsppropdg  14480  qusrhm  14513  mopnset  14537  psrval  14651  fnpsr  14652  psrbasg  14659  psrelbas  14660  psrplusgg  14663  psraddcl  14665  psr0cl  14666  psrnegcl  14668  psr1clfi  14673  mplvalcoe  14675  fnmpl  14678  mplplusgg  14688  vtxvalg  15838  vtxex  15840