![]() |
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 4939 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantr 261 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | fndm 4941 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | eleq2d 2104 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | biimpar 281 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | funfni.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 2, 5, 6 | syl2anc 391 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 df-clel 2033 df-fn 4848 |
This theorem is referenced by: fneu 4946 fnbrfvb 5157 fvelrnb 5164 fvelimab 5172 fniinfv 5174 fvco2 5185 eqfnfv 5208 fndmdif 5215 fndmin 5217 elpreima 5229 fniniseg 5230 fniniseg2 5232 fnniniseg2 5233 rexsupp 5234 fnopfv 5240 fnfvelrn 5242 rexrn 5247 ralrn 5248 fsn2 5280 fnressn 5292 eufnfv 5332 rexima 5337 ralima 5338 fniunfv 5344 dff13 5350 foeqcnvco 5373 f1eqcocnv 5374 isocnv2 5395 isoini 5400 f1oiso 5408 fnovex 5481 suppssof1 5670 offveqb 5672 1stexg 5736 2ndexg 5737 smoiso 5858 rdgruledefgg 5902 rdgivallem 5908 frectfr 5924 frecrdg 5931 freccl 5932 en1 6215 |
Copyright terms: Public domain | W3C validator |