Theorem funfni 5231

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 5228	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 274	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5230	. . . 4 |- ( F Fn A -> dom F = A )
4	3	eleq2d 2210	. . 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 409	1 |- ( ( F Fn A /\ B e. A ) -> ph )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1481   dom cdm 4547   Fun wfun 5125   Fn wfn 5126

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136  df-fn 5134

This theorem is referenced by:  fneu  5235  fnbrfvb  5470  fvelrnb  5477  fvelimab  5485  fniinfv  5487  fvco2  5498  eqfnfv  5526  fndmdif  5533  fndmin  5535  elpreima  5547  fniniseg  5548  fniniseg2  5550  fnniniseg2  5551  rexsupp  5552  fnopfv  5558  fnfvelrn  5560  rexrn  5565  ralrn  5566  fsn2  5602  fnressn  5614  eufnfv  5656  rexima  5664  ralima  5665  fniunfv  5671  dff13  5677  foeqcnvco  5699  f1eqcocnv  5700  isocnv2  5721  isoini  5727  f1oiso  5735  fnovex  5812  suppssof1  6007  offveqb  6009  1stexg  6073  2ndexg  6074  smoiso  6207  rdgruledefgg  6280  rdgivallem  6286  frectfr  6305  frecrdg  6313  en1  6701  fnfi  6833  ordiso2  6928  cc2lem  7098  slotex  12025