![]() |
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 2282 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1509 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | vtoclga.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | vtoclga.2 | . 2 ⊢ (𝑥 ∈ 𝐵 → 𝜑) | |
5 | 1, 2, 3, 4 | vtoclgaf 2754 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1332 ∈ wcel 1481 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-v 2691 |
This theorem is referenced by: vtoclri 2764 ssuni 3766 ordtriexmid 4445 onsucsssucexmid 4450 tfis3 4508 fvmpt3 5508 fvmptssdm 5513 fnressn 5614 fressnfv 5615 caovord 5950 caovimo 5972 tfrlem1 6213 nnacl 6384 nnmcl 6385 nnacom 6388 nnaass 6389 nndi 6390 nnmass 6391 nnmsucr 6392 nnmcom 6393 nnsucsssuc 6396 nntri3or 6397 nnaordi 6412 nnaword 6415 nnmordi 6420 nnaordex 6431 ixpfn 6606 findcard 6790 findcard2 6791 findcard2s 6792 exmidomni 7022 indpi 7174 prarloclem3 7329 uzind4s2 9413 cnref1o 9469 frec2uzrdg 10213 expcl2lemap 10336 seq3coll 10617 climub 11145 climserle 11146 fsum3cvg 11179 summodclem2a 11182 prodfap0 11346 prodfrecap 11347 fproddccvg 11373 alginv 11764 algcvg 11765 algcvga 11768 algfx 11769 prmind2 11837 |
Copyright terms: Public domain | W3C validator |