Theorem funfni 5486

Description: Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.)

Hypothesis

Ref	Expression
funfni.1	|- ( ( Fun F /\ B e. dom F ) -> ph )

Assertion

Ref	Expression
funfni	|- ( ( F Fn A /\ B e. A ) -> ph )

Proof of Theorem funfni

Step	Hyp	Ref	Expression
1		fnfun 5481	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 276	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5483	. . . 4 |- ( F Fn A -> dom F = A )
4	3	eleq2d 2308	. . 3 |- ( F Fn A -> ( B e. dom F <-> B e. A ) )
5	4	biimpar 297	. 2 |- ( ( F Fn A /\ B e. A ) -> B e. dom F )
6		funfni.1	. 2 |- ( ( Fun F /\ B e. dom F ) -> ph )
7	2, 5, 6	syl2anc 415	1 |- ( ( F Fn A /\ B e. A ) -> ph )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. 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  7090  fnfi  7254  ordiso2  7381  cc2lem  7638  slotex  13437  ressbas2d  13481  ressbasid  13483  strressid  13484  ressval3d  13485  imasex  13685  imasival  13686  imasbas  13687  imasplusg  13688  imasmulr  13689  imasaddfn  13697  imasaddval  13698  imasaddf  13699  imasmulfn  13700  imasmulval  13701  imasmulf  13702  qusval  13703  qusex  13705  qusaddvallemg  13713  qusaddflemg  13714  qusaddval  13715  qusaddf  13716  qusmulval  13717  qusmulf  13718  xpsfeq  13725  ismgm  13736  plusffvalg  13741  grpidvalg  13752  fn0g  13754  fngzsum  13767  gzsumvalx  13768  gzsumfzval  13770  gzsumress  13771  gzsum0  13772  issgrp  13777  ismnddef  13790  issubmnd  13814  ress0g  13815  ismhm  13827  mhmex  13828  issubm  13838  0mhm  13852  grppropstrg  13883  grpinvfvalg  13906  grpinvval  13907  grpinvfng  13908  grpsubfvalg  13909  grpsubval  13910  grpressid  13925  grplactfval  13965  qusgrp2  13975  mulgfvalg  13983  mulgval  13984  mulgex  13985  mulgfng  13986  issubg  14035  subgex  14038  issubg2m  14051  isnsg  14064  releqgg  14082  eqgex  14083  eqgfval  14084  eqgen  14089  isghm  14105  cntzex  14150  cntrval  14151  cntzfval  14152  cntzval  14153  ablressid  14229  prdsex  14279  prdsval  14280  prdsbaslemss  14281  prdsbas  14283  prdsplusg  14284  prdsmulr  14285  xpsval  14308  pwsbas  14312  pwselbasb  14313  pwssnf1o  14318  mgptopng  14335  isrng  14340  rngressid  14360  qusrng  14364  dfur2g  14373  issrg  14376  isring  14411  ringidss  14441  ringressid  14477  qusring2  14480  dvdsrvald  14509  dvdsrex  14514  unitgrp  14532  unitabl  14533  invrfvald  14538  unitlinv  14542  unitrinv  14543  dvrfvald  14549  rdivmuldivd  14560  invrpropdg  14565  dfrhm2  14570  rhmex  14573  rhmunitinv  14594  isnzr2  14600  issubrng  14616  issubrg  14638  subrgugrp  14657  rrgval  14679  isdomn  14687  aprval  14700  aprap  14707  aprprop  14710  islmod  14736  scaffvalg  14752  rmodislmod  14797  lssex  14800  lsssetm  14802  islssm  14803  islssmg  14804  islss3  14825  lspfval  14834  lspval  14836  lspcl  14837  lspex  14841  sraval  14883  sralemg  14884  srascag  14888  sravscag  14889  sraipg  14890  sraex  14892  rlmsubg  14904  rlmvnegg  14911  ixpsnbasval  14912  lidlex  14919  rspex  14920  lidlss  14922  lidlrsppropdg  14941  qusrhm  14974  mopnset  14998  aspval  15124  asclfval  15130  psrval  15159  fnpsr  15160  psrbasg  15178  psrelbas  15179  psrplusgg  15182  psraddcl  15184  psrmulrg  15186  psrmulclfilem  15189  psr0cl  15191  psrnegcl  15193  psr1clfi  15198  psrlidmfi  15199  mplvalcoe  15206  fnmpl  15209  mplplusgg  15219  vtxvalg  16462  vtxex  16464