![]() |
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 2253 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfv 1489 |
. 2
![]() ![]() ![]() ![]() | |
3 | vtoclg.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | vtoclg.2 |
. 2
![]() ![]() | |
5 | 1, 2, 3, 4 | vtoclgf 2713 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 |
This theorem depends on definitions: df-bi 116 df-tru 1315 df-nf 1418 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-v 2657 |
This theorem is referenced by: vtoclbg 2716 ceqex 2780 mo2icl 2830 nelrdva 2858 sbctt 2941 sbcnestgf 3015 csbing 3247 ifmdc 3473 prnzg 3611 sneqrg 3653 unisng 3717 csbopabg 3964 trss 3993 inex1g 4022 ssexg 4025 pwexg 4062 prexg 4091 opth 4117 ordelord 4261 uniexg 4319 vtoclr 4545 resieq 4785 csbima12g 4856 dmsnsnsng 4972 iota5 5064 csbiotag 5072 funmo 5094 fconstg 5275 funfveu 5386 funbrfv 5412 fnbrfvb 5414 fvelimab 5429 ssimaexg 5435 fvelrn 5503 isoselem 5673 csbriotag 5694 csbov123g 5761 ovg 5861 tfrexlem 6182 rdg0g 6236 ensn1g 6642 fundmeng 6652 xpdom2g 6676 phplem3g 6700 prcdnql 7233 prcunqu 7234 prdisj 7241 shftvalg 10494 shftval4g 10495 climshft 10958 telfsumo 11120 fsumparts 11124 lcmgcdlem 11597 fiinopn 12007 bdzfauscl 12767 bdinex1g 12778 bdssexg 12781 bj-prexg 12788 bj-uniexg 12795 |
Copyright terms: Public domain | W3C validator |