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

Definition df-fn 5137
 Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-fn (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

Detailed syntax breakdown of Definition df-fn
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2wfn 5129 . 2 wff 𝐴 Fn 𝐵
41wfun 5128 . . 3 wff Fun 𝐴
51cdm 4550 . . . 4 class dom 𝐴
65, 2wceq 1332 . . 3 wff dom 𝐴 = 𝐵
74, 6wa 103 . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
83, 7wb 104 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
 Colors of variables: wff set class This definition is referenced by:  funfn  5164  fnsng  5181  fnprg  5189  fntpg  5190  fntp  5191  fncnv  5200  fneq1  5222  fneq2  5223  nffn  5230  fnfun  5231  fndm  5233  fnun  5240  fnco  5242  fnssresb  5246  fnres  5250  fnresi  5251  fn0  5253  fnopabg  5257  sbcfng  5281  fcoi1  5314  f00  5325  f1cnvcnv  5350  fores  5365  dff1o4  5386  foimacnv  5396  fun11iun  5399  funfvdm  5495  respreima  5559  fpr  5613  fnex  5653  fliftf  5711  fnoprabg  5883  tposfn2  6174  tfrlemibfn  6236  tfri1d  6243  tfr1onlembfn  6252  tfri1dALT  6259  tfrcllembfn  6265  sbthlemi9  6869  caseinl  6992  caseinr  6993  ctssdccl  7012  exmidfodomrlemim  7084  axaddf  7727  axmulf  7728  frecuzrdgtcl  10243  frecuzrdgtclt  10252  shftfn  10655  fntopon  12264
 Copyright terms: Public domain W3C validator