Theorem funfni 5423

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 5418	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 276	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5420	. . . 4 |- ( F Fn A -> dom F = A )
4	3	eleq2d 2299	. . 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 2200   dom cdm 4719   Fun wfun 5312   Fn wfn 5313

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-fn 5321

This theorem is referenced by:  fneu  5427  fnbrfvb  5674  fvelrnb  5683  fvelimab  5692  fniinfv  5694  fvco2  5705  eqfnfv  5734  fndmdif  5742  fndmin  5744  elpreima  5756  fniniseg  5757  fniniseg2  5759  fnniniseg2  5760  rexsupp  5761  fnopfv  5767  fnfvelrn  5769  rexrn  5774  ralrn  5775  fsn2  5811  fnressn  5829  eufnfv  5874  rexima  5884  ralima  5885  fniunfv  5892  dff13  5898  foeqcnvco  5920  f1eqcocnv  5921  isocnv2  5942  isoini  5948  f1oiso  5956  fnovex  6040  suppssof1  6242  offveqb  6244  1stexg  6319  2ndexg  6320  smoiso  6454  rdgruledefgg  6527  rdgivallem  6533  frectfr  6552  frecrdg  6560  en1  6959  fnfi  7114  ordiso2  7213  cc2lem  7463  slotex  13074  ressbas2d  13116  ressbasid  13118  strressid  13119  ressval3d  13120  prdsex  13317  prdsval  13321  prdsbaslemss  13322  prdsbas  13324  prdsplusg  13325  prdsmulr  13326  pwsbas  13340  pwselbasb  13341  pwssnf1o  13346  imasex  13353  imasival  13354  imasbas  13355  imasplusg  13356  imasmulr  13357  imasaddfn  13365  imasaddval  13366  imasaddf  13367  imasmulfn  13368  imasmulval  13369  imasmulf  13370  qusval  13371  qusex  13373  qusaddvallemg  13381  qusaddflemg  13382  qusaddval  13383  qusaddf  13384  qusmulval  13385  qusmulf  13386  xpsfeq  13393  xpsval  13400  ismgm  13405  plusffvalg  13410  grpidvalg  13421  fn0g  13423  fngsum  13436  igsumvalx  13437  gsumfzval  13439  gsumress  13443  gsum0g  13444  issgrp  13451  ismnddef  13466  issubmnd  13490  ress0g  13491  ismhm  13509  mhmex  13510  issubm  13520  0mhm  13534  grppropstrg  13567  grpinvfvalg  13590  grpinvval  13591  grpinvfng  13592  grpsubfvalg  13593  grpsubval  13594  grpressid  13609  grplactfval  13649  qusgrp2  13665  mulgfvalg  13673  mulgval  13674  mulgex  13675  mulgfng  13676  issubg  13725  subgex  13728  issubg2m  13741  isnsg  13754  releqgg  13772  eqgex  13773  eqgfval  13774  eqgen  13779  isghm  13795  ablressid  13887  mgptopng  13907  isrng  13912  rngressid  13932  qusrng  13936  dfur2g  13940  issrg  13943  isring  13978  ringidss  14007  ringressid  14041  qusring2  14044  dvdsrvald  14072  dvdsrex  14077  unitgrp  14095  unitabl  14096  invrfvald  14101  unitlinv  14105  unitrinv  14106  dvrfvald  14112  rdivmuldivd  14123  invrpropdg  14128  dfrhm2  14133  rhmex  14136  rhmunitinv  14157  isnzr2  14163  issubrng  14178  issubrg  14200  subrgugrp  14219  rrgval  14241  isdomn  14248  aprval  14261  aprap  14265  islmod  14270  scaffvalg  14285  rmodislmod  14330  lssex  14333  lsssetm  14335  islssm  14336  islssmg  14337  islss3  14358  lspfval  14367  lspval  14369  lspcl  14370  lspex  14374  sraval  14416  sralemg  14417  srascag  14421  sravscag  14422  sraipg  14423  sraex  14425  rlmsubg  14437  rlmvnegg  14444  ixpsnbasval  14445  lidlex  14452  rspex  14453  lidlss  14455  lidlrsppropdg  14474  qusrhm  14507  mopnset  14531  psrval  14645  fnpsr  14646  psrbasg  14653  psrelbas  14654  psrplusgg  14657  psraddcl  14659  psr0cl  14660  psrnegcl  14662  psr1clfi  14667  mplvalcoe  14669  fnmpl  14672  mplplusgg  14682  vtxvalg  15832  vtxex  15834