![]() |
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 1467 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfv 1467 |
. 2
![]() ![]() ![]() ![]() | |
3 | rspc2v.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | rspc2v.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | rspc2 2733 |
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 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ral 2365 df-v 2622 |
This theorem is referenced by: rspc2va 2736 rspc3v 2738 disji2 3844 wetriext 4405 f1veqaeq 5562 isorel 5601 fovcl 5764 caovclg 5811 caovcomg 5814 smoel 6079 dcdifsnid 6277 unfiexmid 6682 fiintim 6693 supmoti 6742 supsnti 6754 isotilem 6755 cauappcvgprlem1 7272 caucvgprlemnkj 7279 caucvgprlemnbj 7280 caucvgprprlemval 7301 ltordlem 8014 frecuzrdgrrn 9869 frec2uzrdg 9870 frecuzrdgrcl 9871 frecuzrdgrclt 9876 iseqcaopr3 9964 iseqhomo 9996 seq3homo 9998 climcn2 10752 inopn 11756 basis1 11799 basis2 11800 cncfi 11900 |
Copyright terms: Public domain | W3C validator |