![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > vtoclga | GIF version |
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
vtoclga.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtoclga.2 | ⊢ (𝑥 ∈ 𝐵 → 𝜑) |
Ref | Expression |
---|---|
vtoclga | ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2329 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1538 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | vtoclga.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | vtoclga.2 | . 2 ⊢ (𝑥 ∈ 𝐵 → 𝜑) | |
5 | 1, 2, 3, 4 | vtoclgaf 2814 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 = wceq 1363 ∈ wcel 2158 |
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 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-v 2751 |
This theorem is referenced by: vtoclri 2824 ssuni 3843 ordtriexmid 4532 onsucsssucexmid 4538 tfis3 4597 fvmpt3 5608 fvmptssdm 5613 fnressn 5715 fressnfv 5716 caovord 6060 caovimo 6082 tfrlem1 6323 nnacl 6495 nnmcl 6496 nnacom 6499 nnaass 6500 nndi 6501 nnmass 6502 nnmsucr 6503 nnmcom 6504 nnsucsssuc 6507 nntri3or 6508 nnaordi 6523 nnaword 6526 nnmordi 6531 nnaordex 6543 ixpfn 6718 findcard 6902 findcard2 6903 findcard2s 6904 exmidomni 7154 indpi 7355 prarloclem3 7510 uzind4s2 9605 cnref1o 9664 frec2uzrdg 10423 expcl2lemap 10546 seq3coll 10836 climub 11366 climserle 11367 fsum3cvg 11400 summodclem2a 11403 prodfap0 11567 prodfrecap 11568 fproddccvg 11594 alginv 12061 algcvg 12062 algcvga 12065 algfx 12066 prmind2 12134 prmpwdvds 12367 lgsdir2lem4 14785 |
Copyright terms: Public domain | W3C validator |