![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > funfn | GIF version |
Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.) |
Ref | Expression |
---|---|
funfn | ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2082 | . . 3 ⊢ dom 𝐴 = dom 𝐴 | |
2 | 1 | biantru 296 | . 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) |
3 | df-fn 4929 | . 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) | |
4 | 2, 3 | bitr4i 185 | 1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ↔ wb 103 = wceq 1285 dom cdm 4365 Fun wfun 4920 Fn wfn 4921 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-gen 1379 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-cleq 2075 df-fn 4929 |
This theorem is referenced by: funssxp 5085 funforn 5138 funbrfvb 5242 funopfvb 5243 ssimaex 5260 fvco 5269 eqfunfv 5296 fvimacnvi 5307 unpreima 5318 respreima 5321 elrnrexdm 5332 elrnrexdmb 5333 ffvresb 5354 resfunexg 5408 funex 5410 elunirn 5431 smores 5935 smores2 5937 tfrlem1 5951 fundmfibi 6438 fclim 10260 |
Copyright terms: Public domain | W3C validator |