Theorem funfni 5298

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 5295	. . 3 |- ( F Fn A -> Fun F )
2	1	adantr 274	. 2 |- ( ( F Fn A /\ B e. A ) -> Fun F )
3		fndm 5297	. . . 4 |- ( F Fn A -> dom F = A )
4	3	eleq2d 2240	. . 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 2141   dom cdm 4611   Fun wfun 5192   Fn wfn 5193

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166  df-fn 5201

This theorem is referenced by:  fneu  5302  fnbrfvb  5537  fvelrnb  5544  fvelimab  5552  fniinfv  5554  fvco2  5565  eqfnfv  5593  fndmdif  5601  fndmin  5603  elpreima  5615  fniniseg  5616  fniniseg2  5618  fnniniseg2  5619  rexsupp  5620  fnopfv  5626  fnfvelrn  5628  rexrn  5633  ralrn  5634  fsn2  5670  fnressn  5682  eufnfv  5726  rexima  5734  ralima  5735  fniunfv  5741  dff13  5747  foeqcnvco  5769  f1eqcocnv  5770  isocnv2  5791  isoini  5797  f1oiso  5805  fnovex  5886  suppssof1  6078  offveqb  6080  1stexg  6146  2ndexg  6147  smoiso  6281  rdgruledefgg  6354  rdgivallem  6360  frectfr  6379  frecrdg  6387  en1  6777  fnfi  6914  ordiso2  7012  cc2lem  7228  slotex  12443  ismgm  12611  plusffvalg  12616  grpidvalg  12627  fn0g  12629  issgrp  12644  ismnddef  12654  ismhm  12685  issubm  12695  0mhm  12704  grpinvfvalg  12745  grpinvval  12746  grpinvfng  12747  grpsubfvalg  12748  grpsubval  12749