Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > vtoclga | Unicode version |
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
vtoclga.1 | |
vtoclga.2 |
Ref | Expression |
---|---|
vtoclga |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2299 | . 2 | |
2 | nfv 1508 | . 2 | |
3 | vtoclga.1 | . 2 | |
4 | vtoclga.2 | . 2 | |
5 | 1, 2, 3, 4 | vtoclgaf 2777 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1335 wcel 2128 |
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 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-v 2714 |
This theorem is referenced by: vtoclri 2787 ssuni 3794 ordtriexmid 4480 onsucsssucexmid 4486 tfis3 4545 fvmpt3 5547 fvmptssdm 5552 fnressn 5653 fressnfv 5654 caovord 5992 caovimo 6014 tfrlem1 6255 nnacl 6427 nnmcl 6428 nnacom 6431 nnaass 6432 nndi 6433 nnmass 6434 nnmsucr 6435 nnmcom 6436 nnsucsssuc 6439 nntri3or 6440 nnaordi 6455 nnaword 6458 nnmordi 6463 nnaordex 6474 ixpfn 6649 findcard 6833 findcard2 6834 findcard2s 6835 exmidomni 7085 indpi 7262 prarloclem3 7417 uzind4s2 9502 cnref1o 9559 frec2uzrdg 10308 expcl2lemap 10431 seq3coll 10713 climub 11241 climserle 11242 fsum3cvg 11275 summodclem2a 11278 prodfap0 11442 prodfrecap 11443 fproddccvg 11469 alginv 11924 algcvg 11925 algcvga 11928 algfx 11929 prmind2 11997 |
Copyright terms: Public domain | W3C validator |