Theorem funfni 5296

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 5293	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 274	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5295	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2240	. . 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 2141  dom cdm 4609  Fun wfun 5190   Fn wfn 5191

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 5199

This theorem is referenced by:  fneu  5300  fnbrfvb  5535  fvelrnb  5542  fvelimab  5550  fniinfv  5552  fvco2  5563  eqfnfv  5591  fndmdif  5598  fndmin  5600  elpreima  5612  fniniseg  5613  fniniseg2  5615  fnniniseg2  5616  rexsupp  5617  fnopfv  5623  fnfvelrn  5625  rexrn  5630  ralrn  5631  fsn2  5667  fnressn  5679  eufnfv  5723  rexima  5731  ralima  5732  fniunfv  5738  dff13  5744  foeqcnvco  5766  f1eqcocnv  5767  isocnv2  5788  isoini  5794  f1oiso  5802  fnovex  5883  suppssof1  6075  offveqb  6077  1stexg  6143  2ndexg  6144  smoiso  6278  rdgruledefgg  6351  rdgivallem  6357  frectfr  6376  frecrdg  6384  en1  6773  fnfi  6910  ordiso2  7008  cc2lem  7215  slotex  12430  ismgm  12597  plusffvalg  12602  grpidvalg  12613  fn0g  12615  issgrp  12630  ismnddef  12640  ismhm  12671  issubm  12681  0mhm  12690