Theorem funfni 5483

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 5478	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 276	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5480	. . . 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 4774   Fun wfun 5371   Fn wfn 5372

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 5380

This theorem is used by:  fneu  5487  fnbrfvb  5741  fvelrnb  5750  fvelimab  5759  fniinfv  5761  fvco2  5774  eqfnfv  5806  fndmdif  5814  fndmin  5816  elpreima  5828  fniniseg  5829  fniniseg2  5831  fnniniseg2  5832  fnopfv  5838  fnfvelrn  5840  rexrn  5845  ralrn  5846  fsn2  5882  fnressn  5901  eufnfv  5949  rexima  5960  ralima  5961  fniunfv  5968  dff13  5974  foeqcnvco  5996  f1eqcocnv  5997  isocnv2  6018  isoini  6024  f1oiso  6032  fnovex  6118  suppssof1  6320  offveqb  6322  1stexg  6401  2ndexg  6402  smoiso  6573  rdgruledefgg  6646  rdgivallem  6652  frectfr  6671  frecrdg  6679  en1  7086  fnfi  7250  ordiso2  7375  cc2lem  7632  slotex  13379  ressbas2d  13422  ressbasid  13424  strressid  13425  ressval3d  13426  imasex  13626  imasival  13627  imasbas  13628  imasplusg  13629  imasmulr  13630  imasaddfn  13638  imasaddval  13639  imasaddf  13640  imasmulfn  13641  imasmulval  13642  imasmulf  13643  qusval  13644  qusex  13646  qusaddvallemg  13654  qusaddflemg  13655  qusaddval  13656  qusaddf  13657  qusmulval  13658  qusmulf  13659  xpsfeq  13666  ismgm  13677  plusffvalg  13682  grpidvalg  13693  fn0g  13695  fngzsum  13708  gzsumvalx  13709  gzsumfzval  13711  gzsumress  13712  gzsum0  13713  issgrp  13718  ismnddef  13731  issubmnd  13755  ress0g  13756  ismhm  13768  mhmex  13769  issubm  13779  0mhm  13793  grppropstrg  13824  grpinvfvalg  13847  grpinvval  13848  grpinvfng  13849  grpsubfvalg  13850  grpsubval  13851  grpressid  13866  grplactfval  13906  qusgrp2  13916  mulgfvalg  13924  mulgval  13925  mulgex  13926  mulgfng  13927  issubg  13976  subgex  13979  issubg2m  13992  isnsg  14005  releqgg  14023  eqgex  14024  eqgfval  14025  eqgen  14030  isghm  14046  ablressid  14139  prdsex  14172  prdsval  14173  prdsbaslemss  14174  prdsbas  14176  prdsplusg  14177  prdsmulr  14178  xpsval  14201  pwsbas  14205  pwselbasb  14206  pwssnf1o  14211  mgptopng  14228  isrng  14233  rngressid  14253  qusrng  14257  dfur2g  14266  issrg  14269  isring  14304  ringidss  14334  ringressid  14368  qusring2  14371  dvdsrvald  14400  dvdsrex  14405  unitgrp  14423  unitabl  14424  invrfvald  14429  unitlinv  14433  unitrinv  14434  dvrfvald  14440  rdivmuldivd  14451  invrpropdg  14456  dfrhm2  14461  rhmex  14464  rhmunitinv  14485  isnzr2  14491  issubrng  14507  issubrg  14529  subrgugrp  14548  rrgval  14570  isdomn  14578  aprval  14591  aprap  14598  aprprop  14601  islmod  14627  scaffvalg  14643  rmodislmod  14688  lssex  14691  lsssetm  14693  islssm  14694  islssmg  14695  islss3  14716  lspfval  14725  lspval  14727  lspcl  14728  lspex  14732  sraval  14774  sralemg  14775  srascag  14779  sravscag  14780  sraipg  14781  sraex  14783  rlmsubg  14795  rlmvnegg  14802  ixpsnbasval  14803  lidlex  14810  rspex  14811  lidlss  14813  lidlrsppropdg  14832  qusrhm  14865  mopnset  14889  aspval  15015  asclfval  15021  psrval  15050  fnpsr  15051  psrbasg  15065  psrelbas  15066  psrplusgg  15069  psraddcl  15071  psr0cl  15072  psrnegcl  15074  psr1clfi  15079  mplvalcoe  15081  fnmpl  15084  mplplusgg  15094  vtxvalg  16257  vtxex  16259