![]() |
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 2229 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1467 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | vtoclg.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | vtoclg.2 | . 2 ⊢ 𝜑 | |
5 | 1, 2, 3, 4 | vtoclgf 2680 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1290 ∈ wcel 1439 |
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 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-v 2624 |
This theorem is referenced by: vtoclbg 2683 ceqex 2747 mo2icl 2797 nelrdva 2825 sbctt 2908 sbcnestgf 2982 csbing 3210 ifmdc 3434 prnzg 3572 sneqrg 3614 unisng 3678 csbopabg 3924 trss 3953 inex1g 3983 ssexg 3986 pwexg 4023 prexg 4049 opth 4075 ordelord 4219 uniexg 4277 vtoclr 4501 resieq 4738 csbima12g 4808 dmsnsnsng 4923 iota5 5015 csbiotag 5023 funmo 5045 fconstg 5222 funfveu 5333 funbrfv 5358 fnbrfvb 5360 fvelimab 5375 ssimaexg 5381 fvelrn 5446 isoselem 5615 csbriotag 5636 csbov123g 5703 ovg 5799 tfrexlem 6115 rdg0g 6169 ensn1g 6570 fundmeng 6580 xpdom2g 6604 phplem3g 6628 prcdnql 7106 prcunqu 7107 prdisj 7114 shftvalg 10333 shftval4g 10334 climshft 10755 telfsumo 10923 fsumparts 10927 lcmgcdlem 11400 fiinopn 11766 bdzfauscl 12085 bdinex1g 12096 bdssexg 12099 bj-prexg 12106 bj-uniexg 12113 |
Copyright terms: Public domain | W3C validator |