Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > vtoclg1f | Structured version Visualization version GIF version |
Description: Version of vtoclgf 3469 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 2161 and ax-13 2371. (Contributed by BJ, 1-May-2019.) |
Ref | Expression |
---|---|
vtoclg1f.nf | ⊢ Ⅎ𝑥𝜓 |
vtoclg1f.maj | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtoclg1f.min | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtoclg1f | ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisset 2814 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
2 | vtoclg1f.nf | . . 3 ⊢ Ⅎ𝑥𝜓 | |
3 | vtoclg1f.min | . . . 4 ⊢ 𝜑 | |
4 | vtoclg1f.maj | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
5 | 3, 4 | mpbii 236 | . . 3 ⊢ (𝑥 = 𝐴 → 𝜓) |
6 | 2, 5 | exlimi 2218 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓) |
7 | 1, 6 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1542 ∃wex 1786 Ⅎwnf 1790 ∈ wcel 2113 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-12 2178 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-nf 1791 df-sb 2074 df-clab 2717 df-clel 2811 |
This theorem is referenced by: vtoclgOLD 3472 ceqsexg 3550 elabg 3573 mob 3617 opeliunxp2 5682 fvopab5 6808 opeliunxp2f 7906 fprodsplit1f 15437 cnextfvval 22817 dvfsumlem2 24779 dvfsumlem4 24781 bnj981 32501 dmrelrnrel 42295 fmul01 42655 fmuldfeq 42658 fmul01lt1lem1 42659 stoweidlem3 43078 stoweidlem26 43101 stoweidlem31 43106 stoweidlem43 43118 stoweidlem51 43126 fourierdlem86 43267 fourierdlem89 43270 fourierdlem91 43272 salpreimagelt 43776 salpreimalegt 43778 |
Copyright terms: Public domain | W3C validator |