Theorem funfni 5218

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 5215	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 274	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5217	. . . 4 |- ( F Fn A -> dom F = A )
4	3	eleq2d 2207	. . 3 |- ( F Fn A -> ( B e. dom F <-> B e. A ) )
5	4	biimpar 295	. 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 408	1 |- ( ( F Fn A /\ B e. A ) -> ph )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1480   dom cdm 4534   Fun wfun 5112   Fn wfn 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133  df-fn 5121

This theorem is referenced by:  fneu  5222  fnbrfvb  5455  fvelrnb  5462  fvelimab  5470  fniinfv  5472  fvco2  5483  eqfnfv  5511  fndmdif  5518  fndmin  5520  elpreima  5532  fniniseg  5533  fniniseg2  5535  fnniniseg2  5536  rexsupp  5537  fnopfv  5543  fnfvelrn  5545  rexrn  5550  ralrn  5551  fsn2  5587  fnressn  5599  eufnfv  5641  rexima  5649  ralima  5650  fniunfv  5656  dff13  5662  foeqcnvco  5684  f1eqcocnv  5685  isocnv2  5706  isoini  5712  f1oiso  5720  fnovex  5797  suppssof1  5992  offveqb  5994  1stexg  6058  2ndexg  6059  smoiso  6192  rdgruledefgg  6265  rdgivallem  6271  frectfr  6290  frecrdg  6298  en1  6686  fnfi  6818  ordiso2  6913  slotex  11975