Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > vtoclg1f | Structured version Visualization version GIF version |
Description: Version of vtoclgf 3563 with one non-freeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 2151 and ax-13 2381. (Contributed by BJ, 1-May-2019.) |
Ref | Expression |
---|---|
vtoclg1f.nf | ⊢ Ⅎ𝑥𝜓 |
vtoclg1f.maj | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtoclg1f.min | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtoclg1f | ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisset 3503 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
2 | vtoclg1f.nf | . . 3 ⊢ Ⅎ𝑥𝜓 | |
3 | vtoclg1f.min | . . . 4 ⊢ 𝜑 | |
4 | vtoclg1f.maj | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
5 | 3, 4 | mpbii 234 | . . 3 ⊢ (𝑥 = 𝐴 → 𝜓) |
6 | 2, 5 | exlimi 2207 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓) |
7 | 1, 6 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∃wex 1771 Ⅎwnf 1775 ∈ wcel 2105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-nf 1776 df-cleq 2811 df-clel 2890 |
This theorem is referenced by: vtoclg 3565 ceqsexg 3643 elabg 3663 mob 3705 opeliunxp2 5702 fvopab5 6792 opeliunxp2f 7865 fprodsplit1f 15332 cnextfvval 22601 dvfsumlem2 24551 dvfsumlem4 24553 bnj981 32121 dmrelrnrel 41366 fmul01 41737 fmuldfeq 41740 fmul01lt1lem1 41741 stoweidlem3 42165 stoweidlem26 42188 stoweidlem31 42193 stoweidlem43 42205 stoweidlem51 42213 fourierdlem86 42354 fourierdlem89 42357 fourierdlem91 42359 salpreimagelt 42863 salpreimalegt 42865 |
Copyright terms: Public domain | W3C validator |