Theorem funfni 5422

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 5417	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 276	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5419	. . . 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 4718   Fun wfun 5311   Fn wfn 5312

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 5320

This theorem is referenced by:  fneu  5426  fnbrfvb  5671  fvelrnb  5680  fvelimab  5689  fniinfv  5691  fvco2  5702  eqfnfv  5731  fndmdif  5739  fndmin  5741  elpreima  5753  fniniseg  5754  fniniseg2  5756  fnniniseg2  5757  rexsupp  5758  fnopfv  5764  fnfvelrn  5766  rexrn  5771  ralrn  5772  fsn2  5808  fnressn  5824  eufnfv  5869  rexima  5877  ralima  5878  fniunfv  5885  dff13  5891  foeqcnvco  5913  f1eqcocnv  5914  isocnv2  5935  isoini  5941  f1oiso  5949  fnovex  6033  suppssof1  6234  offveqb  6236  1stexg  6311  2ndexg  6312  smoiso  6446  rdgruledefgg  6519  rdgivallem  6525  frectfr  6544  frecrdg  6552  en1  6949  fnfi  7099  ordiso2  7198  cc2lem  7448  slotex  13054  ressbas2d  13096  ressbasid  13098  strressid  13099  ressval3d  13100  prdsex  13297  prdsval  13301  prdsbaslemss  13302  prdsbas  13304  prdsplusg  13305  prdsmulr  13306  pwsbas  13320  pwselbasb  13321  pwssnf1o  13326  imasex  13333  imasival  13334  imasbas  13335  imasplusg  13336  imasmulr  13337  imasaddfn  13345  imasaddval  13346  imasaddf  13347  imasmulfn  13348  imasmulval  13349  imasmulf  13350  qusval  13351  qusex  13353  qusaddvallemg  13361  qusaddflemg  13362  qusaddval  13363  qusaddf  13364  qusmulval  13365  qusmulf  13366  xpsfeq  13373  xpsval  13380  ismgm  13385  plusffvalg  13390  grpidvalg  13401  fn0g  13403  fngsum  13416  igsumvalx  13417  gsumfzval  13419  gsumress  13423  gsum0g  13424  issgrp  13431  ismnddef  13446  issubmnd  13470  ress0g  13471  ismhm  13489  mhmex  13490  issubm  13500  0mhm  13514  grppropstrg  13547  grpinvfvalg  13570  grpinvval  13571  grpinvfng  13572  grpsubfvalg  13573  grpsubval  13574  grpressid  13589  grplactfval  13629  qusgrp2  13645  mulgfvalg  13653  mulgval  13654  mulgex  13655  mulgfng  13656  issubg  13705  subgex  13708  issubg2m  13721  isnsg  13734  releqgg  13752  eqgex  13753  eqgfval  13754  eqgen  13759  isghm  13775  ablressid  13867  mgptopng  13887  isrng  13892  rngressid  13912  qusrng  13916  dfur2g  13920  issrg  13923  isring  13958  ringidss  13987  ringressid  14021  qusring2  14024  reldvdsrsrg  14050  dvdsrvald  14051  dvdsrex  14056  unitgrp  14074  unitabl  14075  invrfvald  14080  unitlinv  14084  unitrinv  14085  dvrfvald  14091  rdivmuldivd  14102  invrpropdg  14107  dfrhm2  14112  rhmex  14115  rhmunitinv  14136  isnzr2  14142  issubrng  14157  issubrg  14179  subrgugrp  14198  rrgval  14220  isdomn  14227  aprval  14240  aprap  14244  islmod  14249  scaffvalg  14264  rmodislmod  14309  lssex  14312  lsssetm  14314  islssm  14315  islssmg  14316  islss3  14337  lspfval  14346  lspval  14348  lspcl  14349  lspex  14353  sraval  14395  sralemg  14396  srascag  14400  sravscag  14401  sraipg  14402  sraex  14404  rlmsubg  14416  rlmvnegg  14423  ixpsnbasval  14424  lidlex  14431  rspex  14432  lidlss  14434  lidlrsppropdg  14453  qusrhm  14486  mopnset  14510  psrval  14624  fnpsr  14625  psrbasg  14632  psrelbas  14633  psrplusgg  14636  psraddcl  14638  psr0cl  14639  psrnegcl  14641  psr1clfi  14646  mplvalcoe  14648  fnmpl  14651  mplplusgg  14661  vtxvalg  15811  vtxex  15813