Theorem funfni 5385

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 5380	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 276	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5382	. . . 4 |- ( F Fn A -> dom F = A )
4	3	eleq2d 2276	. . 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 2177   dom cdm 4683   Fun wfun 5274   Fn wfn 5275

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202  df-fn 5283

This theorem is referenced by:  fneu  5389  fnbrfvb  5632  fvelrnb  5639  fvelimab  5648  fniinfv  5650  fvco2  5661  eqfnfv  5690  fndmdif  5698  fndmin  5700  elpreima  5712  fniniseg  5713  fniniseg2  5715  fnniniseg2  5716  rexsupp  5717  fnopfv  5723  fnfvelrn  5725  rexrn  5730  ralrn  5731  fsn2  5767  fnressn  5783  eufnfv  5828  rexima  5836  ralima  5837  fniunfv  5844  dff13  5850  foeqcnvco  5872  f1eqcocnv  5873  isocnv2  5894  isoini  5900  f1oiso  5908  fnovex  5990  suppssof1  6189  offveqb  6191  1stexg  6266  2ndexg  6267  smoiso  6401  rdgruledefgg  6474  rdgivallem  6480  frectfr  6499  frecrdg  6507  en1  6904  fnfi  7053  ordiso2  7152  cc2lem  7398  slotex  12934  ressbas2d  12975  ressbasid  12977  strressid  12978  ressval3d  12979  prdsex  13176  prdsval  13180  prdsbaslemss  13181  prdsbas  13183  prdsplusg  13184  prdsmulr  13185  pwsbas  13199  pwselbasb  13200  pwssnf1o  13205  imasex  13212  imasival  13213  imasbas  13214  imasplusg  13215  imasmulr  13216  imasaddfn  13224  imasaddval  13225  imasaddf  13226  imasmulfn  13227  imasmulval  13228  imasmulf  13229  qusval  13230  qusex  13232  qusaddvallemg  13240  qusaddflemg  13241  qusaddval  13242  qusaddf  13243  qusmulval  13244  qusmulf  13245  xpsfeq  13252  xpsval  13259  ismgm  13264  plusffvalg  13269  grpidvalg  13280  fn0g  13282  fngsum  13295  igsumvalx  13296  gsumfzval  13298  gsumress  13302  gsum0g  13303  issgrp  13310  ismnddef  13325  issubmnd  13349  ress0g  13350  ismhm  13368  mhmex  13369  issubm  13379  0mhm  13393  grppropstrg  13426  grpinvfvalg  13449  grpinvval  13450  grpinvfng  13451  grpsubfvalg  13452  grpsubval  13453  grpressid  13468  grplactfval  13508  qusgrp2  13524  mulgfvalg  13532  mulgval  13533  mulgex  13534  mulgfng  13535  issubg  13584  subgex  13587  issubg2m  13600  isnsg  13613  releqgg  13631  eqgex  13632  eqgfval  13633  eqgen  13638  isghm  13654  ablressid  13746  mgptopng  13766  isrng  13771  rngressid  13791  qusrng  13795  dfur2g  13799  issrg  13802  isring  13837  ringidss  13866  ringressid  13900  qusring2  13903  reldvdsrsrg  13929  dvdsrvald  13930  dvdsrex  13935  unitgrp  13953  unitabl  13954  invrfvald  13959  unitlinv  13963  unitrinv  13964  dvrfvald  13970  rdivmuldivd  13981  invrpropdg  13986  dfrhm2  13991  rhmex  13994  rhmunitinv  14015  isnzr2  14021  issubrng  14036  issubrg  14058  subrgugrp  14077  rrgval  14099  isdomn  14106  aprval  14119  aprap  14123  islmod  14128  scaffvalg  14143  rmodislmod  14188  lssex  14191  lsssetm  14193  islssm  14194  islssmg  14195  islss3  14216  lspfval  14225  lspval  14227  lspcl  14228  lspex  14232  sraval  14274  sralemg  14275  srascag  14279  sravscag  14280  sraipg  14281  sraex  14283  rlmsubg  14295  rlmvnegg  14302  ixpsnbasval  14303  lidlex  14310  rspex  14311  lidlss  14313  lidlrsppropdg  14332  qusrhm  14365  mopnset  14389  psrval  14503  fnpsr  14504  psrbasg  14511  psrelbas  14512  psrplusgg  14515  psraddcl  14517  psr0cl  14518  psrnegcl  14520  psr1clfi  14525  mplvalcoe  14527  fnmpl  14530  mplplusgg  14540  vtxvalg  15690  vtxex  15692