![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > vtoclg | GIF 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: → wi 4 ↔ wb 105 = wceq 1364 ∈ wcel 2160 |
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 4195 prexg 4226 opth 4252 ordelord 4396 uniexg 4454 vtoclr 4689 resieq 4932 csbima12g 5004 dmsnsnsng 5121 iota5 5213 csbiotag 5224 funmo 5246 fconstg 5427 funfveu 5543 funbrfv 5570 fnbrfvb 5572 fvelimab 5588 ssimaexg 5594 fvelrn 5663 isoselem 5837 csbriotag 5859 csbov123g 5929 ovg 6030 tfrexlem 6353 rdg0g 6407 ensn1g 6815 fundmeng 6825 xpdom2g 6850 phplem3g 6874 prcdnql 7501 prcunqu 7502 prdisj 7509 shftvalg 10863 shftval4g 10864 climshft 11330 telfsumo 11492 fsumparts 11496 lcmgcdlem 12095 fiinopn 13888 bdzfauscl 15026 bdinex1g 15037 bdssexg 15040 bj-prexg 15047 bj-uniexg 15054 |
Copyright terms: Public domain | W3C validator |