Theorem funfni 5318

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 5315	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 276	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5317	. . . 4 |- ( F Fn A -> dom F = A )
4	3	eleq2d 2247	. . 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 2148   dom cdm 4628   Fun wfun 5212   Fn wfn 5213

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-fn 5221

This theorem is referenced by:  fneu  5322  fnbrfvb  5558  fvelrnb  5565  fvelimab  5574  fniinfv  5576  fvco2  5587  eqfnfv  5615  fndmdif  5623  fndmin  5625  elpreima  5637  fniniseg  5638  fniniseg2  5640  fnniniseg2  5641  rexsupp  5642  fnopfv  5648  fnfvelrn  5650  rexrn  5655  ralrn  5656  fsn2  5692  fnressn  5704  eufnfv  5749  rexima  5757  ralima  5758  fniunfv  5765  dff13  5771  foeqcnvco  5793  f1eqcocnv  5794  isocnv2  5815  isoini  5821  f1oiso  5829  fnovex  5910  suppssof1  6102  offveqb  6104  1stexg  6170  2ndexg  6171  smoiso  6305  rdgruledefgg  6378  rdgivallem  6384  frectfr  6403  frecrdg  6411  en1  6801  fnfi  6938  ordiso2  7036  cc2lem  7267  slotex  12491  ressbas2d  12530  strressid  12532  ressval3d  12533  prdsex  12723  imasex  12731  imasival  12732  imasbas  12733  imasplusg  12734  imasmulr  12735  imasaddfn  12743  imasaddval  12744  imasaddf  12745  imasmulfn  12746  imasmulval  12747  imasmulf  12748  qusval  12749  qusaddvallemg  12757  qusaddflemg  12758  qusaddval  12759  qusaddf  12760  qusmulval  12761  qusmulf  12762  xpsfeq  12769  xpsval  12776  ismgm  12781  plusffvalg  12786  grpidvalg  12797  fn0g  12799  issgrp  12814  ismnddef  12824  issubmnd  12848  ress0g  12849  ismhm  12858  issubm  12868  0mhm  12878  grppropstrg  12900  grpinvfvalg  12920  grpinvval  12921  grpinvfng  12922  grpsubfvalg  12923  grpsubval  12924  grpressid  12936  grplactfval  12976  mulgfvalg  12990  mulgval  12991  mulgfng  12992  issubg  13038  subgex  13041  issubg2m  13054  isnsg  13067  releqgg  13085  eqgfval  13086  eqgen  13091  mgptopng  13144  dfur2g  13150  issrg  13153  isring  13188  ringidss  13217  ringressid  13243  reldvdsrsrg  13266  dvdsrvald  13267  dvdsrex  13272  unitgrp  13290  unitabl  13291  invrfvald  13296  unitlinv  13300  unitrinv  13301  dvrfvald  13307  rdivmuldivd  13318  invrpropdg  13323  issubrg  13347  subrgugrp  13366  aprval  13377  aprap  13381  islmod  13386  scaffvalg  13401  rmodislmod  13446  lsssetm  13449  islssm  13450  islss3  13471  lspfval  13480  lspval  13482  lspcl  13483