Theorem funfni 5439

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 5434	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 276	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5436	. . . 4 |- ( F Fn A -> dom F = A )
4	3	eleq2d 2301	. . 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 2202   dom cdm 4731   Fun wfun 5327   Fn wfn 5328

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-fn 5336

This theorem is referenced by:  fneu  5443  fnbrfvb  5693  fvelrnb  5702  fvelimab  5711  fniinfv  5713  fvco2  5724  eqfnfv  5753  fndmdif  5761  fndmin  5763  elpreima  5775  fniniseg  5776  fniniseg2  5778  fnniniseg2  5779  fnopfv  5785  fnfvelrn  5787  rexrn  5792  ralrn  5793  fsn2  5829  fnressn  5848  eufnfv  5895  rexima  5905  ralima  5906  fniunfv  5913  dff13  5919  foeqcnvco  5941  f1eqcocnv  5942  isocnv2  5963  isoini  5969  f1oiso  5977  fnovex  6061  suppssof1  6262  offveqb  6264  1stexg  6339  2ndexg  6340  smoiso  6511  rdgruledefgg  6584  rdgivallem  6590  frectfr  6609  frecrdg  6617  en1  7016  fnfi  7178  ordiso2  7277  cc2lem  7528  slotex  13172  ressbas2d  13214  ressbasid  13216  strressid  13217  ressval3d  13218  prdsex  13415  prdsval  13419  prdsbaslemss  13420  prdsbas  13422  prdsplusg  13423  prdsmulr  13424  pwsbas  13438  pwselbasb  13439  pwssnf1o  13444  imasex  13451  imasival  13452  imasbas  13453  imasplusg  13454  imasmulr  13455  imasaddfn  13463  imasaddval  13464  imasaddf  13465  imasmulfn  13466  imasmulval  13467  imasmulf  13468  qusval  13469  qusex  13471  qusaddvallemg  13479  qusaddflemg  13480  qusaddval  13481  qusaddf  13482  qusmulval  13483  qusmulf  13484  xpsfeq  13491  xpsval  13498  ismgm  13503  plusffvalg  13508  grpidvalg  13519  fn0g  13521  fngsum  13534  igsumvalx  13535  gsumfzval  13537  gsumress  13541  gsum0g  13542  issgrp  13549  ismnddef  13564  issubmnd  13588  ress0g  13589  ismhm  13607  mhmex  13608  issubm  13618  0mhm  13632  grppropstrg  13665  grpinvfvalg  13688  grpinvval  13689  grpinvfng  13690  grpsubfvalg  13691  grpsubval  13692  grpressid  13707  grplactfval  13747  qusgrp2  13763  mulgfvalg  13771  mulgval  13772  mulgex  13773  mulgfng  13774  issubg  13823  subgex  13826  issubg2m  13839  isnsg  13852  releqgg  13870  eqgex  13871  eqgfval  13872  eqgen  13877  isghm  13893  ablressid  13985  mgptopng  14006  isrng  14011  rngressid  14031  qusrng  14035  dfur2g  14039  issrg  14042  isring  14077  ringidss  14106  ringressid  14140  qusring2  14143  dvdsrvald  14171  dvdsrex  14176  unitgrp  14194  unitabl  14195  invrfvald  14200  unitlinv  14204  unitrinv  14205  dvrfvald  14211  rdivmuldivd  14222  invrpropdg  14227  dfrhm2  14232  rhmex  14235  rhmunitinv  14256  isnzr2  14262  issubrng  14277  issubrg  14299  subrgugrp  14318  rrgval  14340  isdomn  14348  aprval  14361  aprap  14365  islmod  14370  scaffvalg  14385  rmodislmod  14430  lssex  14433  lsssetm  14435  islssm  14436  islssmg  14437  islss3  14458  lspfval  14467  lspval  14469  lspcl  14470  lspex  14474  sraval  14516  sralemg  14517  srascag  14521  sravscag  14522  sraipg  14523  sraex  14525  rlmsubg  14537  rlmvnegg  14544  ixpsnbasval  14545  lidlex  14552  rspex  14553  lidlss  14555  lidlrsppropdg  14574  qusrhm  14607  mopnset  14631  psrval  14745  fnpsr  14746  psrbasg  14758  psrelbas  14759  psrplusgg  14762  psraddcl  14764  psr0cl  14765  psrnegcl  14767  psr1clfi  14772  mplvalcoe  14774  fnmpl  14777  mplplusgg  14787  vtxvalg  15940  vtxex  15942