![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vtoclg1f | Structured version Visualization version GIF version |
Description: Version of vtoclgf 3522 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-10 2138 and ax-11 2155. (Contributed by BJ, 1-May-2019.) |
Ref | Expression |
---|---|
vtoclg1f.nf | ⊢ Ⅎ𝑥𝜓 |
vtoclg1f.maj | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtoclg1f.min | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtoclg1f | ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisset 2816 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
2 | vtoclg1f.nf | . . 3 ⊢ Ⅎ𝑥𝜓 | |
3 | vtoclg1f.min | . . . 4 ⊢ 𝜑 | |
4 | vtoclg1f.maj | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
5 | 3, 4 | mpbii 232 | . . 3 ⊢ (𝑥 = 𝐴 → 𝜓) |
6 | 2, 5 | exlimi 2211 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓) |
7 | 1, 6 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ∃wex 1782 Ⅎwnf 1786 ∈ wcel 2107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-clel 2811 |
This theorem is referenced by: vtoclgOLDOLD 3526 ceqsexg 3604 elabgOLD 3630 mob 3676 opeliunxp2 5795 fvopab5 6981 opeliunxp2f 8142 fprodsplit1f 15878 cnextfvval 23432 dvfsumlem2 25407 dvfsumlem4 25409 bnj981 33619 dmrelrnrel 43534 fmul01 43907 fmuldfeq 43910 fmul01lt1lem1 43911 stoweidlem3 44330 stoweidlem26 44353 stoweidlem31 44358 stoweidlem43 44370 stoweidlem51 44378 fourierdlem86 44519 fourierdlem89 44522 fourierdlem91 44524 salpreimagelt 45034 salpreimalegt 45036 |
Copyright terms: Public domain | W3C validator |