Theorem funfni 5288

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 5285	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 274	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5287	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2236	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	4	biimpar 295	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ dom 𝐹)
6		funfni.1	. 2 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑)
7	2, 5, 6	syl2anc 409	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2136  dom cdm 4604  Fun wfun 5182   Fn wfn 5183

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161  df-fn 5191

This theorem is referenced by:  fneu  5292  fnbrfvb  5527  fvelrnb  5534  fvelimab  5542  fniinfv  5544  fvco2  5555  eqfnfv  5583  fndmdif  5590  fndmin  5592  elpreima  5604  fniniseg  5605  fniniseg2  5607  fnniniseg2  5608  rexsupp  5609  fnopfv  5615  fnfvelrn  5617  rexrn  5622  ralrn  5623  fsn2  5659  fnressn  5671  eufnfv  5715  rexima  5723  ralima  5724  fniunfv  5730  dff13  5736  foeqcnvco  5758  f1eqcocnv  5759  isocnv2  5780  isoini  5786  f1oiso  5794  fnovex  5875  suppssof1  6067  offveqb  6069  1stexg  6135  2ndexg  6136  smoiso  6270  rdgruledefgg  6343  rdgivallem  6349  frectfr  6368  frecrdg  6376  en1  6765  fnfi  6902  ordiso2  7000  cc2lem  7207  slotex  12421  ismgm  12588  plusffvalg  12593  grpidvalg  12604  fn0g  12606  issgrp  12621