![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vtoclg1f | Structured version Visualization version GIF version |
Description: Version of vtoclgf 3465 with one non-freeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 2150 and ax-13 2334. (Contributed by BJ, 1-May-2019.) |
Ref | Expression |
---|---|
vtoclg1f.nf | ⊢ Ⅎ𝑥𝜓 |
vtoclg1f.maj | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtoclg1f.min | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtoclg1f | ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3414 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | isset 3409 | . . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
3 | vtoclg1f.nf | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
4 | vtoclg1f.min | . . . . 5 ⊢ 𝜑 | |
5 | vtoclg1f.maj | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
6 | 4, 5 | mpbii 225 | . . . 4 ⊢ (𝑥 = 𝐴 → 𝜓) |
7 | 3, 6 | exlimi 2203 | . . 3 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓) |
8 | 2, 7 | sylbi 209 | . 2 ⊢ (𝐴 ∈ V → 𝜓) |
9 | 1, 8 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1601 ∃wex 1823 Ⅎwnf 1827 ∈ wcel 2107 Vcvv 3398 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-v 3400 |
This theorem is referenced by: vtoclg 3467 ceqsexg 3537 elabg 3556 mob 3600 opeliunxp2 5506 fvopab5 6572 opeliunxp2f 7618 fprodsplit1f 15123 cnextfvval 22277 dvfsumlem2 24227 dvfsumlem4 24229 bnj981 31619 dmrelrnrel 40340 fmul01 40720 fmuldfeq 40723 fmul01lt1lem1 40724 stoweidlem3 41147 stoweidlem26 41170 stoweidlem31 41175 stoweidlem43 41187 stoweidlem51 41195 fourierdlem86 41336 fourierdlem89 41339 fourierdlem91 41341 |
Copyright terms: Public domain | W3C validator |