![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rspc2v | Unicode version |
Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.) |
Ref | Expression |
---|---|
rspc2v.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
rspc2v.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rspc2v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1539 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfv 1539 |
. 2
![]() ![]() ![]() ![]() | |
3 | rspc2v.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | rspc2v.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | rspc2 2867 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-v 2754 |
This theorem is referenced by: rspc2va 2870 rspc3v 2872 disji2 4011 ontriexmidim 4539 wetriext 4594 f1veqaeq 5791 isorel 5830 oveqrspc2v 5923 fovcld 6001 caovclg 6049 caovcomg 6052 smoel 6325 dcdifsnid 6529 unfiexmid 6946 fiintim 6957 supmoti 7022 supsnti 7034 isotilem 7035 onntri35 7266 onntri45 7270 cauappcvgprlem1 7688 caucvgprlemnkj 7695 caucvgprlemnbj 7696 caucvgprprlemval 7717 ltordlem 8469 frecuzrdgrrn 10439 frec2uzrdg 10440 frecuzrdgrcl 10441 frecuzrdgrclt 10446 seq3caopr3 10512 seq3homo 10541 climcn2 11349 fprodcl2lem 11645 ennnfonelemim 12475 mhmlin 12919 issubg2m 13128 nsgbi 13143 ghmlin 13187 issubrng2 13557 issubrg2 13588 lmodlema 13608 islmodd 13609 rmodislmodlem 13666 rmodislmod 13667 rnglidlmcl 13796 inopn 13963 basis1 14007 basis2 14008 xmeteq0 14319 cncfi 14525 limccnp2lem 14605 logltb 14755 2sqlem8 14931 redcwlpo 15265 redc0 15267 reap0 15268 |
Copyright terms: Public domain | W3C validator |