Theorem funfni 5478

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 5473	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 276	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5475	. . . 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 )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2209   dom cdm 4769   Fun wfun 5366   Fn wfn 5367

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234  df-fn 5375

This theorem is referenced by:  fneu  5482  fnbrfvb  5735  fvelrnb  5744  fvelimab  5753  fniinfv  5755  fvco2  5768  eqfnfv  5797  fndmdif  5805  fndmin  5807  elpreima  5819  fniniseg  5820  fniniseg2  5822  fnniniseg2  5823  fnopfv  5829  fnfvelrn  5831  rexrn  5836  ralrn  5837  fsn2  5873  fnressn  5892  eufnfv  5939  rexima  5950  ralima  5951  fniunfv  5958  dff13  5964  foeqcnvco  5986  f1eqcocnv  5987  isocnv2  6008  isoini  6014  f1oiso  6022  fnovex  6108  suppssof1  6310  offveqb  6312  1stexg  6391  2ndexg  6392  smoiso  6563  rdgruledefgg  6636  rdgivallem  6642  frectfr  6661  frecrdg  6669  en1  7076  fnfi  7240  ordiso2  7365  cc2lem  7622  slotex  13357  ressbas2d  13399  ressbasid  13401  strressid  13402  ressval3d  13403  imasex  13603  imasival  13604  imasbas  13605  imasplusg  13606  imasmulr  13607  imasaddfn  13615  imasaddval  13616  imasaddf  13617  imasmulfn  13618  imasmulval  13619  imasmulf  13620  qusval  13621  qusex  13623  qusaddvallemg  13631  qusaddflemg  13632  qusaddval  13633  qusaddf  13634  qusmulval  13635  qusmulf  13636  xpsfeq  13643  ismgm  13654  plusffvalg  13659  grpidvalg  13670  fn0g  13672  fngzsum  13685  gzsumvalx  13686  gzsumfzval  13688  gzsumress  13689  gzsum0  13690  issgrp  13695  ismnddef  13708  issubmnd  13732  ress0g  13733  ismhm  13745  mhmex  13746  issubm  13756  0mhm  13770  grppropstrg  13801  grpinvfvalg  13824  grpinvval  13825  grpinvfng  13826  grpsubfvalg  13827  grpsubval  13828  grpressid  13843  grplactfval  13883  qusgrp2  13893  mulgfvalg  13901  mulgval  13902  mulgex  13903  mulgfng  13904  issubg  13953  subgex  13956  issubg2m  13969  isnsg  13982  releqgg  14000  eqgex  14001  eqgfval  14002  eqgen  14007  isghm  14023  ablressid  14116  prdsex  14149  prdsval  14150  prdsbaslemss  14151  prdsbas  14153  prdsplusg  14154  prdsmulr  14155  xpsval  14178  pwsbas  14182  pwselbasb  14183  pwssnf1o  14188  mgptopng  14203  isrng  14208  rngressid  14228  qusrng  14232  dfur2g  14240  issrg  14243  isring  14278  ringidss  14307  ringressid  14341  qusring2  14344  dvdsrvald  14373  dvdsrex  14378  unitgrp  14396  unitabl  14397  invrfvald  14402  unitlinv  14406  unitrinv  14407  dvrfvald  14413  rdivmuldivd  14424  invrpropdg  14429  dfrhm2  14434  rhmex  14437  rhmunitinv  14458  isnzr2  14464  issubrng  14480  issubrg  14502  subrgugrp  14521  rrgval  14543  isdomn  14551  aprval  14564  aprap  14571  aprprop  14574  islmod  14600  scaffvalg  14615  rmodislmod  14660  lssex  14663  lsssetm  14665  islssm  14666  islssmg  14667  islss3  14688  lspfval  14697  lspval  14699  lspcl  14700  lspex  14704  sraval  14746  sralemg  14747  srascag  14751  sravscag  14752  sraipg  14753  sraex  14755  rlmsubg  14767  rlmvnegg  14774  ixpsnbasval  14775  lidlex  14782  rspex  14783  lidlss  14785  lidlrsppropdg  14804  qusrhm  14837  mopnset  14861  psrval  14973  fnpsr  14974  psrbasg  14988  psrelbas  14989  psrplusgg  14992  psraddcl  14994  psr0cl  14995  psrnegcl  14997  psr1clfi  15002  mplvalcoe  15004  fnmpl  15007  mplplusgg  15017  vtxvalg  16171  vtxex  16173