Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rspc | Unicode version |
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.) |
Ref | Expression |
---|---|
rspc.1 | |
rspc.2 |
Ref | Expression |
---|---|
rspc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 2419 | . 2 | |
2 | nfcv 2279 | . . . 4 | |
3 | nfv 1508 | . . . . 5 | |
4 | rspc.1 | . . . . 5 | |
5 | 3, 4 | nfim 1551 | . . . 4 |
6 | eleq1 2200 | . . . . 5 | |
7 | rspc.2 | . . . . 5 | |
8 | 6, 7 | imbi12d 233 | . . . 4 |
9 | 2, 5, 8 | spcgf 2763 | . . 3 |
10 | 9 | pm2.43a 51 | . 2 |
11 | 1, 10 | syl5bi 151 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wal 1329 wceq 1331 wnf 1436 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: rspcv 2780 rspc2 2795 pofun 4229 omsinds 4530 fmptcof 5580 fliftfuns 5692 qliftfuns 6506 xpf1o 6731 finexdc 6789 ssfirab 6815 iunfidisj 6827 lble 8698 exfzdc 10010 uzsinds 10208 sumeq2 11121 sumfct 11136 sumrbdclem 11138 summodclem3 11142 summodclem2a 11143 zsumdc 11146 fsumgcl 11148 fsum3 11149 fsumf1o 11152 isumss 11153 isumss2 11155 fsum3cvg2 11156 fsumadd 11168 isummulc2 11188 fsum2dlemstep 11196 fisumcom2 11200 fsumshftm 11207 fisum0diag2 11209 fsummulc2 11210 fsum00 11224 fsumabs 11227 fsumrelem 11233 fsumiun 11239 isumshft 11252 mertenslem2 11298 prodeq2 11319 prodrbdclem 11333 zsupcllemstep 11627 infssuzex 11631 bezoutlemmain 11675 ctiunctlemudc 11939 iuncld 12273 txcnp 12429 fsumcncntop 12714 bj-nntrans 13138 |
Copyright terms: Public domain | W3C validator |