Theorem funfni 5019

Description: Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.)

Hypothesis

Ref	Expression
funfni.1	⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑)

Assertion

Ref	Expression
funfni	⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑)

Proof of Theorem funfni

Step	Hyp	Ref	Expression
1		fnfun 5016	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 270	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5018	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2148	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	4	biimpar 291	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ dom 𝐹)
6		funfni.1	. 2 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑)
7	2, 5, 6	syl2anc 403	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1433  dom cdm 4363  Fun wfun 4916   Fn wfn 4917

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077  df-fn 4925

This theorem is referenced by:  fneu  5023  fnbrfvb  5235  fvelrnb  5242  fvelimab  5250  fniinfv  5252  fvco2  5263  eqfnfv  5286  fndmdif  5293  fndmin  5295  elpreima  5307  fniniseg  5308  fniniseg2  5310  fnniniseg2  5311  rexsupp  5312  fnopfv  5318  fnfvelrn  5320  rexrn  5325  ralrn  5326  fsn2  5358  fnressn  5370  eufnfv  5410  rexima  5415  ralima  5416  fniunfv  5422  dff13  5428  foeqcnvco  5450  f1eqcocnv  5451  isocnv2  5472  isoini  5477  f1oiso  5485  fnovex  5558  suppssof1  5748  offveqb  5750  1stexg  5814  2ndexg  5815  smoiso  5940  rdgruledefgg  5985  rdgivallem  5991  frectfr  6008  frecrdg  6015  freccl  6016  en1  6302  fnfi  6388  ordiso2  6446