Theorem funfni 5463

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 5458	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 276	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5460	. . . 4 |- ( F Fn A -> dom F = A )
4	3	eleq2d 2304	. . 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 411	1 |- ( ( F Fn A /\ B e. A ) -> ph )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2205   dom cdm 4754   Fun wfun 5351   Fn wfn 5352

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 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230  df-fn 5360

This theorem is referenced by:  fneu  5467  fnbrfvb  5720  fvelrnb  5729  fvelimab  5738  fniinfv  5740  fvco2  5751  eqfnfv  5780  fndmdif  5788  fndmin  5790  elpreima  5802  fniniseg  5803  fniniseg2  5805  fnniniseg2  5806  fnopfv  5812  fnfvelrn  5814  rexrn  5819  ralrn  5820  fsn2  5856  fnressn  5875  eufnfv  5922  rexima  5933  ralima  5934  fniunfv  5941  dff13  5947  foeqcnvco  5969  f1eqcocnv  5970  isocnv2  5991  isoini  5997  f1oiso  6005  fnovex  6091  suppssof1  6293  offveqb  6295  1stexg  6374  2ndexg  6375  smoiso  6546  rdgruledefgg  6619  rdgivallem  6625  frectfr  6644  frecrdg  6652  en1  7052  fnfi  7216  ordiso2  7339  cc2lem  7596  slotex  13323  ressbas2d  13365  ressbasid  13367  strressid  13368  ressval3d  13369  imasex  13569  imasival  13570  imasbas  13571  imasplusg  13572  imasmulr  13573  imasaddfn  13581  imasaddval  13582  imasaddf  13583  imasmulfn  13584  imasmulval  13585  imasmulf  13586  qusval  13587  qusex  13589  qusaddvallemg  13597  qusaddflemg  13598  qusaddval  13599  qusaddf  13600  qusmulval  13601  qusmulf  13602  xpsfeq  13609  ismgm  13620  plusffvalg  13625  grpidvalg  13636  fn0g  13638  fngsum  13651  igsumvalx  13652  gsumfzval  13654  gsumress  13658  gsum0g  13659  issgrp  13666  ismnddef  13679  issubmnd  13703  ress0g  13704  ismhm  13716  mhmex  13717  issubm  13727  0mhm  13741  grppropstrg  13774  grpinvfvalg  13797  grpinvval  13798  grpinvfng  13799  grpsubfvalg  13800  grpsubval  13801  grpressid  13816  grplactfval  13856  qusgrp2  13866  mulgfvalg  13874  mulgval  13875  mulgex  13876  mulgfng  13877  issubg  13926  subgex  13929  issubg2m  13942  isnsg  13955  releqgg  13973  eqgex  13974  eqgfval  13975  eqgen  13980  isghm  13996  ablressid  14088  prdsex  14114  prdsval  14115  prdsbaslemss  14116  prdsbas  14118  prdsplusg  14119  prdsmulr  14120  xpsval  14143  pwsbas  14147  pwselbasb  14148  pwssnf1o  14153  mgptopng  14168  isrng  14173  rngressid  14193  qusrng  14197  dfur2g  14205  issrg  14208  isring  14243  ringidss  14272  ringressid  14306  qusring2  14309  dvdsrvald  14338  dvdsrex  14343  unitgrp  14361  unitabl  14362  invrfvald  14367  unitlinv  14371  unitrinv  14372  dvrfvald  14378  rdivmuldivd  14389  invrpropdg  14394  dfrhm2  14399  rhmex  14402  rhmunitinv  14423  isnzr2  14429  issubrng  14445  issubrg  14467  subrgugrp  14486  rrgval  14508  isdomn  14516  aprval  14529  aprap  14536  aprprop  14539  islmod  14565  scaffvalg  14580  rmodislmod  14625  lssex  14628  lsssetm  14630  islssm  14631  islssmg  14632  islss3  14653  lspfval  14662  lspval  14664  lspcl  14665  lspex  14669  sraval  14711  sralemg  14712  srascag  14716  sravscag  14717  sraipg  14718  sraex  14720  rlmsubg  14732  rlmvnegg  14739  ixpsnbasval  14740  lidlex  14747  rspex  14748  lidlss  14750  lidlrsppropdg  14769  qusrhm  14802  mopnset  14826  psrval  14940  fnpsr  14941  psrbasg  14955  psrelbas  14956  psrplusgg  14959  psraddcl  14961  psr0cl  14962  psrnegcl  14964  psr1clfi  14969  mplvalcoe  14971  fnmpl  14974  mplplusgg  14984  vtxvalg  16137  vtxex  16139