Theorem funfni 5429

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 5424	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 276	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5426	. . . 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 4723   Fun wfun 5318   Fn wfn 5319

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 5327

This theorem is referenced by:  fneu  5433  fnbrfvb  5680  fvelrnb  5689  fvelimab  5698  fniinfv  5700  fvco2  5711  eqfnfv  5740  fndmdif  5748  fndmin  5750  elpreima  5762  fniniseg  5763  fniniseg2  5765  fnniniseg2  5766  rexsupp  5767  fnopfv  5773  fnfvelrn  5775  rexrn  5780  ralrn  5781  fsn2  5817  fnressn  5835  eufnfv  5880  rexima  5890  ralima  5891  fniunfv  5898  dff13  5904  foeqcnvco  5926  f1eqcocnv  5927  isocnv2  5948  isoini  5954  f1oiso  5962  fnovex  6046  suppssof1  6248  offveqb  6250  1stexg  6325  2ndexg  6326  smoiso  6463  rdgruledefgg  6536  rdgivallem  6542  frectfr  6561  frecrdg  6569  en1  6968  fnfi  7126  ordiso2  7225  cc2lem  7475  slotex  13099  ressbas2d  13141  ressbasid  13143  strressid  13144  ressval3d  13145  prdsex  13342  prdsval  13346  prdsbaslemss  13347  prdsbas  13349  prdsplusg  13350  prdsmulr  13351  pwsbas  13365  pwselbasb  13366  pwssnf1o  13371  imasex  13378  imasival  13379  imasbas  13380  imasplusg  13381  imasmulr  13382  imasaddfn  13390  imasaddval  13391  imasaddf  13392  imasmulfn  13393  imasmulval  13394  imasmulf  13395  qusval  13396  qusex  13398  qusaddvallemg  13406  qusaddflemg  13407  qusaddval  13408  qusaddf  13409  qusmulval  13410  qusmulf  13411  xpsfeq  13418  xpsval  13425  ismgm  13430  plusffvalg  13435  grpidvalg  13446  fn0g  13448  fngsum  13461  igsumvalx  13462  gsumfzval  13464  gsumress  13468  gsum0g  13469  issgrp  13476  ismnddef  13491  issubmnd  13515  ress0g  13516  ismhm  13534  mhmex  13535  issubm  13545  0mhm  13559  grppropstrg  13592  grpinvfvalg  13615  grpinvval  13616  grpinvfng  13617  grpsubfvalg  13618  grpsubval  13619  grpressid  13634  grplactfval  13674  qusgrp2  13690  mulgfvalg  13698  mulgval  13699  mulgex  13700  mulgfng  13701  issubg  13750  subgex  13753  issubg2m  13766  isnsg  13779  releqgg  13797  eqgex  13798  eqgfval  13799  eqgen  13804  isghm  13820  ablressid  13912  mgptopng  13932  isrng  13937  rngressid  13957  qusrng  13961  dfur2g  13965  issrg  13968  isring  14003  ringidss  14032  ringressid  14066  qusring2  14069  dvdsrvald  14097  dvdsrex  14102  unitgrp  14120  unitabl  14121  invrfvald  14126  unitlinv  14130  unitrinv  14131  dvrfvald  14137  rdivmuldivd  14148  invrpropdg  14153  dfrhm2  14158  rhmex  14161  rhmunitinv  14182  isnzr2  14188  issubrng  14203  issubrg  14225  subrgugrp  14244  rrgval  14266  isdomn  14273  aprval  14286  aprap  14290  islmod  14295  scaffvalg  14310  rmodislmod  14355  lssex  14358  lsssetm  14360  islssm  14361  islssmg  14362  islss3  14383  lspfval  14392  lspval  14394  lspcl  14395  lspex  14399  sraval  14441  sralemg  14442  srascag  14446  sravscag  14447  sraipg  14448  sraex  14450  rlmsubg  14462  rlmvnegg  14469  ixpsnbasval  14470  lidlex  14477  rspex  14478  lidlss  14480  lidlrsppropdg  14499  qusrhm  14532  mopnset  14556  psrval  14670  fnpsr  14671  psrbasg  14678  psrelbas  14679  psrplusgg  14682  psraddcl  14684  psr0cl  14685  psrnegcl  14687  psr1clfi  14692  mplvalcoe  14694  fnmpl  14697  mplplusgg  14707  vtxvalg  15857  vtxex  15859