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 2312 | . 2 | |
2 | nfv 1521 | . 2 | |
3 | vtoclga.1 | . 2 | |
4 | vtoclga.2 | . 2 | |
5 | 1, 2, 3, 4 | vtoclgaf 2795 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1348 wcel 2141 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-v 2732 |
This theorem is referenced by: vtoclri 2805 ssuni 3818 ordtriexmid 4505 onsucsssucexmid 4511 tfis3 4570 fvmpt3 5575 fvmptssdm 5580 fnressn 5682 fressnfv 5683 caovord 6024 caovimo 6046 tfrlem1 6287 nnacl 6459 nnmcl 6460 nnacom 6463 nnaass 6464 nndi 6465 nnmass 6466 nnmsucr 6467 nnmcom 6468 nnsucsssuc 6471 nntri3or 6472 nnaordi 6487 nnaword 6490 nnmordi 6495 nnaordex 6507 ixpfn 6682 findcard 6866 findcard2 6867 findcard2s 6868 exmidomni 7118 indpi 7304 prarloclem3 7459 uzind4s2 9550 cnref1o 9609 frec2uzrdg 10365 expcl2lemap 10488 seq3coll 10777 climub 11307 climserle 11308 fsum3cvg 11341 summodclem2a 11344 prodfap0 11508 prodfrecap 11509 fproddccvg 11535 alginv 12001 algcvg 12002 algcvga 12005 algfx 12006 prmind2 12074 prmpwdvds 12307 lgsdir2lem4 13726 |
Copyright terms: Public domain | W3C validator |