Theorem funfni 5317

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 5314	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 276	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5316	. . . 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 4627  Fun wfun 5211   Fn wfn 5212

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 5220

This theorem is referenced by:  fneu  5321  fnbrfvb  5557  fvelrnb  5564  fvelimab  5573  fniinfv  5575  fvco2  5586  eqfnfv  5614  fndmdif  5622  fndmin  5624  elpreima  5636  fniniseg  5637  fniniseg2  5639  fnniniseg2  5640  rexsupp  5641  fnopfv  5647  fnfvelrn  5649  rexrn  5654  ralrn  5655  fsn2  5691  fnressn  5703  eufnfv  5748  rexima  5756  ralima  5757  fniunfv  5763  dff13  5769  foeqcnvco  5791  f1eqcocnv  5792  isocnv2  5813  isoini  5819  f1oiso  5827  fnovex  5908  suppssof1  6100  offveqb  6102  1stexg  6168  2ndexg  6169  smoiso  6303  rdgruledefgg  6376  rdgivallem  6382  frectfr  6401  frecrdg  6409  en1  6799  fnfi  6936  ordiso2  7034  cc2lem  7265  slotex  12489  ressbas2d  12528  strressid  12530  ressval3d  12531  prdsex  12718  imasex  12726  imasival  12727  imasbas  12728  imasplusg  12729  imasmulr  12730  imasaddfn  12738  imasaddval  12739  imasaddf  12740  imasmulfn  12741  imasmulval  12742  imasmulf  12743  qusval  12744  qusaddvallemg  12752  qusaddflemg  12753  qusaddval  12754  qusaddf  12755  qusmulval  12756  qusmulf  12757  xpsfeq  12764  xpsval  12771  ismgm  12776  plusffvalg  12781  grpidvalg  12792  fn0g  12794  issgrp  12809  ismnddef  12819  issubmnd  12843  ress0g  12844  ismhm  12853  issubm  12863  0mhm  12873  grppropstrg  12895  grpinvfvalg  12915  grpinvval  12916  grpinvfng  12917  grpsubfvalg  12918  grpsubval  12919  grpressid  12931  grplactfval  12971  mulgfvalg  12985  mulgval  12986  mulgfng  12987  issubg  13033  subgex  13036  issubg2m  13049  isnsg  13062  releqgg  13080  eqgfval  13081  eqgen  13086  mgptopng  13139  dfur2g  13145  issrg  13148  isring  13183  ringidss  13212  ringressid  13238  reldvdsrsrg  13261  dvdsrvald  13262  dvdsrex  13267  unitgrp  13285  unitabl  13286  invrfvald  13291  unitlinv  13295  unitrinv  13296  dvrfvald  13302  rdivmuldivd  13313  invrpropdg  13318  issubrg  13342  subrgugrp  13361  aprval  13372  aprap  13376  islmod  13381  scaffvalg  13396  rmodislmod  13441