Theorem funfni 4942

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 4939	. . 3 |- ( F Fn A -> Fun F)
2	1	adantr 261	. 2 |- (( F Fn A /\ B e. A) -> Fun F)
3		fndm 4941	. . . 4 |- ( F Fn A -> dom F = A)
4	3	eleq2d 2104	. . 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 1390   dom cdm 4288   Fun wfun 4839   Fn wfn 4840

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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033  df-fn 4848

This theorem is referenced by:  fneu  4946  fnbrfvb  5157  fvelrnb  5164  fvelimab  5172  fniinfv  5174  fvco2  5185  eqfnfv  5208  fndmdif  5215  fndmin  5217  elpreima  5229  fniniseg  5230  fniniseg2  5232  fnniniseg2  5233  rexsupp  5234  fnopfv  5240  fnfvelrn  5242  rexrn  5247  ralrn  5248  fsn2  5280  fnressn  5292  eufnfv  5332  rexima  5337  ralima  5338  fniunfv  5344  dff13  5350  foeqcnvco  5373  f1eqcocnv  5374  isocnv2  5395  isoini  5400  f1oiso  5408  fnovex  5481  suppssof1  5670  offveqb  5672  1stexg  5736  2ndexg  5737  smoiso  5858  rdgruledefgg  5902  rdgivallem  5908  frectfr  5924  frecrdg  5931  freccl  5932  en1  6215