ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  funfni GIF version

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
StepHypRef Expression
1 fnfun 5293 . . 3 (𝐹 Fn 𝐴 → Fun 𝐹)
21adantr 274 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → Fun 𝐹)
3 fndm 5295 . . . 4 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
43eleq2d 2240 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹𝐵𝐴))
54biimpar 295 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → 𝐵 ∈ dom 𝐹)
6 funfni.1 . 2 ((Fun 𝐹𝐵 ∈ dom 𝐹) → 𝜑)
72, 5, 6syl2anc 409 1 ((𝐹 Fn 𝐴𝐵𝐴) → 𝜑)
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator