Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > funfni | Unicode version |
Description: Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.) |
Ref | Expression |
---|---|
funfni.1 |
Ref | Expression |
---|---|
funfni |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnfun 5016 | . . 3 | |
2 | 1 | adantr 270 | . 2 |
3 | fndm 5018 | . . . 4 | |
4 | 3 | eleq2d 2148 | . . 3 |
5 | 4 | biimpar 291 | . 2 |
6 | funfni.1 | . 2 | |
7 | 2, 5, 6 | syl2anc 403 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 102 wcel 1433 cdm 4363 wfun 4916 wfn 4917 |
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-5 1376 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-4 1440 ax-17 1459 ax-ial 1467 ax-ext 2063 |
This theorem depends on definitions: df-bi 115 df-cleq 2074 df-clel 2077 df-fn 4925 |
This theorem is referenced by: fneu 5023 fnbrfvb 5235 fvelrnb 5242 fvelimab 5250 fniinfv 5252 fvco2 5263 eqfnfv 5286 fndmdif 5293 fndmin 5295 elpreima 5307 fniniseg 5308 fniniseg2 5310 fnniniseg2 5311 rexsupp 5312 fnopfv 5318 fnfvelrn 5320 rexrn 5325 ralrn 5326 fsn2 5358 fnressn 5370 eufnfv 5410 rexima 5415 ralima 5416 fniunfv 5422 dff13 5428 foeqcnvco 5450 f1eqcocnv 5451 isocnv2 5472 isoini 5477 f1oiso 5485 fnovex 5558 suppssof1 5748 offveqb 5750 1stexg 5814 2ndexg 5815 smoiso 5940 rdgruledefgg 5985 rdgivallem 5991 frectfr 6008 frecrdg 6015 freccl 6016 en1 6302 fnfi 6388 ordiso2 6446 |
Copyright terms: Public domain | W3C validator |