Theorem funfni 5376

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 5371	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 276	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5373	. . . 4 |- ( F Fn A -> dom F = A )
4	3	eleq2d 2275	. . 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 2176   dom cdm 4675   Fun wfun 5265   Fn wfn 5266

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201  df-fn 5274

This theorem is referenced by:  fneu  5380  fnbrfvb  5619  fvelrnb  5626  fvelimab  5635  fniinfv  5637  fvco2  5648  eqfnfv  5677  fndmdif  5685  fndmin  5687  elpreima  5699  fniniseg  5700  fniniseg2  5702  fnniniseg2  5703  rexsupp  5704  fnopfv  5710  fnfvelrn  5712  rexrn  5717  ralrn  5718  fsn2  5754  fnressn  5770  eufnfv  5815  rexima  5823  ralima  5824  fniunfv  5831  dff13  5837  foeqcnvco  5859  f1eqcocnv  5860  isocnv2  5881  isoini  5887  f1oiso  5895  fnovex  5977  suppssof1  6176  offveqb  6178  1stexg  6253  2ndexg  6254  smoiso  6388  rdgruledefgg  6461  rdgivallem  6467  frectfr  6486  frecrdg  6494  en1  6891  fnfi  7038  ordiso2  7137  cc2lem  7378  slotex  12859  ressbas2d  12900  ressbasid  12902  strressid  12903  ressval3d  12904  prdsex  13101  prdsval  13105  prdsbaslemss  13106  prdsbas  13108  prdsplusg  13109  prdsmulr  13110  pwsbas  13124  pwselbasb  13125  pwssnf1o  13130  imasex  13137  imasival  13138  imasbas  13139  imasplusg  13140  imasmulr  13141  imasaddfn  13149  imasaddval  13150  imasaddf  13151  imasmulfn  13152  imasmulval  13153  imasmulf  13154  qusval  13155  qusex  13157  qusaddvallemg  13165  qusaddflemg  13166  qusaddval  13167  qusaddf  13168  qusmulval  13169  qusmulf  13170  xpsfeq  13177  xpsval  13184  ismgm  13189  plusffvalg  13194  grpidvalg  13205  fn0g  13207  fngsum  13220  igsumvalx  13221  gsumfzval  13223  gsumress  13227  gsum0g  13228  issgrp  13235  ismnddef  13250  issubmnd  13274  ress0g  13275  ismhm  13293  mhmex  13294  issubm  13304  0mhm  13318  grppropstrg  13351  grpinvfvalg  13374  grpinvval  13375  grpinvfng  13376  grpsubfvalg  13377  grpsubval  13378  grpressid  13393  grplactfval  13433  qusgrp2  13449  mulgfvalg  13457  mulgval  13458  mulgex  13459  mulgfng  13460  issubg  13509  subgex  13512  issubg2m  13525  isnsg  13538  releqgg  13556  eqgex  13557  eqgfval  13558  eqgen  13563  isghm  13579  ablressid  13671  mgptopng  13691  isrng  13696  rngressid  13716  qusrng  13720  dfur2g  13724  issrg  13727  isring  13762  ringidss  13791  ringressid  13825  qusring2  13828  reldvdsrsrg  13854  dvdsrvald  13855  dvdsrex  13860  unitgrp  13878  unitabl  13879  invrfvald  13884  unitlinv  13888  unitrinv  13889  dvrfvald  13895  rdivmuldivd  13906  invrpropdg  13911  dfrhm2  13916  rhmex  13919  rhmunitinv  13940  isnzr2  13946  issubrng  13961  issubrg  13983  subrgugrp  14002  rrgval  14024  isdomn  14031  aprval  14044  aprap  14048  islmod  14053  scaffvalg  14068  rmodislmod  14113  lssex  14116  lsssetm  14118  islssm  14119  islssmg  14120  islss3  14141  lspfval  14150  lspval  14152  lspcl  14153  lspex  14157  sraval  14199  sralemg  14200  srascag  14204  sravscag  14205  sraipg  14206  sraex  14208  rlmsubg  14220  rlmvnegg  14227  ixpsnbasval  14228  lidlex  14235  rspex  14236  lidlss  14238  lidlrsppropdg  14257  qusrhm  14290  mopnset  14314  psrval  14428  fnpsr  14429  psrbasg  14436  psrelbas  14437  psrplusgg  14440  psraddcl  14442  psr0cl  14443  psrnegcl  14445  psr1clfi  14450  mplvalcoe  14452  fnmpl  14455  mplplusgg  14465  vtxvalg  15615