Theorem funfni 5313

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 5310	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 276	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5312	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2247	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	4	biimpar 297	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ dom 𝐹)
6		funfni.1	. 2 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑)
7	2, 5, 6	syl2anc 411	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  dom cdm 4624  Fun wfun 5207   Fn wfn 5208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-fn 5216

This theorem is referenced by:  fneu  5317  fnbrfvb  5553  fvelrnb  5560  fvelimab  5569  fniinfv  5571  fvco2  5582  eqfnfv  5610  fndmdif  5618  fndmin  5620  elpreima  5632  fniniseg  5633  fniniseg2  5635  fnniniseg2  5636  rexsupp  5637  fnopfv  5643  fnfvelrn  5645  rexrn  5650  ralrn  5651  fsn2  5687  fnressn  5699  eufnfv  5743  rexima  5751  ralima  5752  fniunfv  5758  dff13  5764  foeqcnvco  5786  f1eqcocnv  5787  isocnv2  5808  isoini  5814  f1oiso  5822  fnovex  5903  suppssof1  6095  offveqb  6097  1stexg  6163  2ndexg  6164  smoiso  6298  rdgruledefgg  6371  rdgivallem  6377  frectfr  6396  frecrdg  6404  en1  6794  fnfi  6931  ordiso2  7029  cc2lem  7260  slotex  12479  ressbas2d  12518  strressid  12520  ressval3d  12521  ismgm  12706  plusffvalg  12711  grpidvalg  12722  fn0g  12724  issgrp  12739  ismnddef  12749  issubmnd  12773  ismhm  12781  issubm  12791  0mhm  12801  grppropstrg  12823  grpinvfvalg  12843  grpinvval  12844  grpinvfng  12845  grpsubfvalg  12846  grpsubval  12847  grpressid  12859  grplactfval  12899  mulgfvalg  12913  mulgval  12914  mulgfng  12915  issubg  12960  issubg2m  12975  mgptopng  13039  dfur2g  13045  issrg  13048  isring  13083  ringidss  13112  reldvdsrsrg  13160  dvdsrvald  13161  dvdsrex  13166  unitgrp  13184  unitabl  13185  invrfvald  13190  unitlinv  13194  unitrinv  13195  dvrfvald  13201  rdivmuldivd  13212  invrpropdg  13217  aprval  13239  aprap  13243