![]() |
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 2332 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfv 1539 |
. 2
![]() ![]() ![]() ![]() | |
3 | vtoclg.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | vtoclg.2 |
. 2
![]() ![]() | |
5 | 1, 2, 3, 4 | vtoclgf 2810 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 |
This theorem is referenced by: vtoclbg 2813 ceqex 2879 mo2icl 2931 nelrdva 2959 sbctt 3044 sbcnestgf 3123 csbing 3357 ifmdc 3589 prnzg 3731 sneqrg 3777 unisng 3841 csbopabg 4096 trss 4125 inex1g 4154 ssexg 4157 pwexg 4198 prexg 4229 opth 4255 ordelord 4399 uniexg 4457 vtoclr 4692 resieq 4935 csbima12g 5007 dmsnsnsng 5124 iotaexab 5214 iota5 5217 csbiotag 5228 funmo 5250 fconstg 5431 funfveu 5547 funbrfv 5575 fnbrfvb 5577 fvelimab 5593 ssimaexg 5599 fvelrn 5668 isoselem 5842 csbriotag 5865 csbov123g 5935 ovg 6036 tfrexlem 6360 rdg0g 6414 ensn1g 6824 fundmeng 6834 xpdom2g 6859 phplem3g 6885 prcdnql 7514 prcunqu 7515 prdisj 7522 shftvalg 10880 shftval4g 10881 climshft 11347 telfsumo 11509 fsumparts 11513 lcmgcdlem 12112 fiinopn 13981 bdzfauscl 15120 bdinex1g 15131 bdssexg 15134 bj-prexg 15141 bj-uniexg 15148 |
Copyright terms: Public domain | W3C validator |