![]() |
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 1528 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfv 1528 |
. 2
![]() ![]() ![]() ![]() | |
3 | rspc2v.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | rspc2v.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | rspc2 2853 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-v 2740 |
This theorem is referenced by: rspc2va 2856 rspc3v 2858 disji2 3997 ontriexmidim 4522 wetriext 4577 f1veqaeq 5770 isorel 5809 oveqrspc2v 5902 fovcl 5980 caovclg 6027 caovcomg 6030 smoel 6301 dcdifsnid 6505 unfiexmid 6917 fiintim 6928 supmoti 6992 supsnti 7004 isotilem 7005 onntri35 7236 onntri45 7240 cauappcvgprlem1 7658 caucvgprlemnkj 7665 caucvgprlemnbj 7666 caucvgprprlemval 7687 ltordlem 8439 frecuzrdgrrn 10408 frec2uzrdg 10409 frecuzrdgrcl 10410 frecuzrdgrclt 10415 seq3caopr3 10481 seq3homo 10510 climcn2 11317 fprodcl2lem 11613 ennnfonelemim 12425 mhmlin 12858 issubg2m 13049 nsgbi 13064 issubrg2 13362 lmodlema 13382 islmodd 13383 rmodislmodlem 13440 rmodislmod 13441 inopn 13506 basis1 13550 basis2 13551 xmeteq0 13862 cncfi 14068 limccnp2lem 14148 logltb 14298 2sqlem8 14473 redcwlpo 14806 redc0 14808 reap0 14809 |
Copyright terms: Public domain | W3C validator |