![]() |
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 2235 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1473 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | vtoclga.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | vtoclga.2 | . 2 ⊢ (𝑥 ∈ 𝐵 → 𝜑) | |
5 | 1, 2, 3, 4 | vtoclgaf 2698 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1296 ∈ wcel 1445 |
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 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 |
This theorem is referenced by: vtoclri 2708 ssuni 3697 ordtriexmid 4366 onsucsssucexmid 4371 tfis3 4429 fvmpt3 5418 fvmptssdm 5423 fnressn 5522 fressnfv 5523 caovord 5854 caovimo 5876 tfrlem1 6111 nnacl 6281 nnmcl 6282 nnacom 6285 nnaass 6286 nndi 6287 nnmass 6288 nnmsucr 6289 nnmcom 6290 nnsucsssuc 6293 nntri3or 6294 nnaordi 6307 nnaword 6310 nnmordi 6315 nnaordex 6326 ixpfn 6501 findcard 6684 findcard2 6685 findcard2s 6686 exmidomni 6885 indpi 6998 prarloclem3 7153 uzind4s2 9178 cnref1o 9232 frec2uzrdg 9965 expcl2lemap 10098 seq3coll 10378 climub 10903 climserle 10904 fsum3cvg 10936 summodclem2a 10940 alginv 11472 algcvg 11473 algcvga 11476 algfx 11477 prmind2 11545 |
Copyright terms: Public domain | W3C validator |