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 1508 | . 2 | |
2 | nfv 1508 | . 2 | |
3 | rspc2v.1 | . 2 | |
4 | rspc2v.2 | . 2 | |
5 | 1, 2, 3, 4 | rspc2 2795 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wceq 1331 wcel 1480 wral 2414 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-ral 2419 df-v 2683 |
This theorem is referenced by: rspc2va 2798 rspc3v 2800 disji2 3917 wetriext 4486 f1veqaeq 5663 isorel 5702 fovcl 5869 caovclg 5916 caovcomg 5919 smoel 6190 dcdifsnid 6393 unfiexmid 6799 fiintim 6810 supmoti 6873 supsnti 6885 isotilem 6886 cauappcvgprlem1 7460 caucvgprlemnkj 7467 caucvgprlemnbj 7468 caucvgprprlemval 7489 ltordlem 8237 frecuzrdgrrn 10174 frec2uzrdg 10175 frecuzrdgrcl 10176 frecuzrdgrclt 10181 seq3caopr3 10247 seq3homo 10276 climcn2 11071 ennnfonelemim 11926 inopn 12159 basis1 12203 basis2 12204 xmeteq0 12517 cncfi 12723 limccnp2lem 12803 |
Copyright terms: Public domain | W3C validator |