Theorem funfni 4999

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 4996	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 261	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 4998	. . . 4 |- ( F Fn A -> dom F = A )
4	3	eleq2d 2107	. . 3 |- ( F Fn A -> ( B e. dom F <-> B e. A ) )
5	4	biimpar 281	. 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 391	1 |- ( ( F Fn A /\ B e. A ) -> ph )

Syntax hints:   -> wi 4   /\ wa 97   e. wcel 1393   dom cdm 4345   Fun wfun 4896   Fn wfn 4897

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036  df-fn 4905

This theorem is referenced by:  fneu  5003  fnbrfvb  5214  fvelrnb  5221  fvelimab  5229  fniinfv  5231  fvco2  5242  eqfnfv  5265  fndmdif  5272  fndmin  5274  elpreima  5286  fniniseg  5287  fniniseg2  5289  fnniniseg2  5290  rexsupp  5291  fnopfv  5297  fnfvelrn  5299  rexrn  5304  ralrn  5305  fsn2  5337  fnressn  5349  eufnfv  5389  rexima  5394  ralima  5395  fniunfv  5401  dff13  5407  foeqcnvco  5430  f1eqcocnv  5431  isocnv2  5452  isoini  5457  f1oiso  5465  fnovex  5538  suppssof1  5728  offveqb  5730  1stexg  5794  2ndexg  5795  smoiso  5917  rdgruledefgg  5962  rdgivallem  5968  frectfr  5985  frecrdg  5992  freccl  5993  en1  6279  ordiso2  6357