Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > vtoclg | Unicode version |
Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) |
Ref | Expression |
---|---|
vtoclg.1 | |
vtoclg.2 |
Ref | Expression |
---|---|
vtoclg |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2281 | . 2 | |
2 | nfv 1508 | . 2 | |
3 | vtoclg.1 | . 2 | |
4 | vtoclg.2 | . 2 | |
5 | 1, 2, 3, 4 | vtoclgf 2744 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1331 wcel 1480 |
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 2121 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-v 2688 |
This theorem is referenced by: vtoclbg 2747 ceqex 2812 mo2icl 2863 nelrdva 2891 sbctt 2975 sbcnestgf 3051 csbing 3283 ifmdc 3509 prnzg 3647 sneqrg 3689 unisng 3753 csbopabg 4006 trss 4035 inex1g 4064 ssexg 4067 pwexg 4104 prexg 4133 opth 4159 ordelord 4303 uniexg 4361 vtoclr 4587 resieq 4829 csbima12g 4900 dmsnsnsng 5016 iota5 5108 csbiotag 5116 funmo 5138 fconstg 5319 funfveu 5434 funbrfv 5460 fnbrfvb 5462 fvelimab 5477 ssimaexg 5483 fvelrn 5551 isoselem 5721 csbriotag 5742 csbov123g 5809 ovg 5909 tfrexlem 6231 rdg0g 6285 ensn1g 6691 fundmeng 6701 xpdom2g 6726 phplem3g 6750 prcdnql 7292 prcunqu 7293 prdisj 7300 shftvalg 10608 shftval4g 10609 climshft 11073 telfsumo 11235 fsumparts 11239 lcmgcdlem 11758 fiinopn 12171 bdzfauscl 13088 bdinex1g 13099 bdssexg 13102 bj-prexg 13109 bj-uniexg 13116 |
Copyright terms: Public domain | W3C validator |