Theorem funfni 5328

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 5325	. . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	adantr 276	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹)
3		fndm 5327	. . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2257	. . 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 2158  dom cdm 4638  Fun wfun 5222   Fn wfn 5223

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183  df-fn 5231

This theorem is referenced by:  fneu  5332  fnbrfvb  5569  fvelrnb  5576  fvelimab  5585  fniinfv  5587  fvco2  5598  eqfnfv  5626  fndmdif  5634  fndmin  5636  elpreima  5648  fniniseg  5649  fniniseg2  5651  fnniniseg2  5652  rexsupp  5653  fnopfv  5659  fnfvelrn  5661  rexrn  5666  ralrn  5667  fsn2  5703  fnressn  5715  eufnfv  5760  rexima  5768  ralima  5769  fniunfv  5776  dff13  5782  foeqcnvco  5804  f1eqcocnv  5805  isocnv2  5826  isoini  5832  f1oiso  5840  fnovex  5921  suppssof1  6113  offveqb  6115  1stexg  6181  2ndexg  6182  smoiso  6316  rdgruledefgg  6389  rdgivallem  6395  frectfr  6414  frecrdg  6422  en1  6812  fnfi  6949  ordiso2  7047  cc2lem  7278  slotex  12502  ressbas2d  12541  ressbasid  12543  strressid  12544  ressval3d  12545  prdsex  12735  imasex  12743  imasival  12744  imasbas  12745  imasplusg  12746  imasmulr  12747  imasaddfn  12755  imasaddval  12756  imasaddf  12757  imasmulfn  12758  imasmulval  12759  imasmulf  12760  qusval  12761  qusex  12763  qusaddvallemg  12770  qusaddflemg  12771  qusaddval  12772  qusaddf  12773  qusmulval  12774  qusmulf  12775  xpsfeq  12782  xpsval  12789  ismgm  12794  plusffvalg  12799  grpidvalg  12810  fn0g  12812  issgrp  12827  ismnddef  12840  issubmnd  12864  ress0g  12865  ismhm  12874  issubm  12884  0mhm  12894  grppropstrg  12916  grpinvfvalg  12938  grpinvval  12939  grpinvfng  12940  grpsubfvalg  12941  grpsubval  12942  grpressid  12957  grplactfval  12997  qusgrp2  13007  mulgfvalg  13015  mulgval  13016  mulgex  13017  mulgfng  13018  issubg  13064  subgex  13067  issubg2m  13080  isnsg  13093  releqgg  13111  eqgex  13112  eqgfval  13113  eqgen  13118  ablressid  13169  mgptopng  13179  isrng  13184  rngressid  13204  dfur2g  13209  issrg  13212  isring  13247  ringidss  13276  ringressid  13306  qusring2  13309  reldvdsrsrg  13335  dvdsrvald  13336  dvdsrex  13341  unitgrp  13359  unitabl  13360  invrfvald  13365  unitlinv  13369  unitrinv  13370  dvrfvald  13376  rdivmuldivd  13387  invrpropdg  13392  issubrng  13414  issubrg  13436  subrgugrp  13455  aprval  13466  aprap  13470  islmod  13475  scaffvalg  13490  rmodislmod  13535  lssex  13538  lsssetm  13540  islssm  13541  islssmg  13542  islss3  13563  lspfval  13572  lspval  13574  lspcl  13575  lspex  13579  sraval  13621  sralemg  13622  srascag  13626  sravscag  13627  sraipg  13628  sraex  13630  rlmsubg  13642  rlmvnegg  13649  ixpsnbasval  13650  lidlex  13657  rspex  13658  lidlss  13660