Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > vtoclg1f | Structured version Visualization version GIF version |
Description: Version of vtoclgf 3503 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 2154 and ax-13 2372. (Contributed by BJ, 1-May-2019.) |
Ref | Expression |
---|---|
vtoclg1f.nf | ⊢ Ⅎ𝑥𝜓 |
vtoclg1f.maj | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtoclg1f.min | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtoclg1f | ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisset 2820 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
2 | vtoclg1f.nf | . . 3 ⊢ Ⅎ𝑥𝜓 | |
3 | vtoclg1f.min | . . . 4 ⊢ 𝜑 | |
4 | vtoclg1f.maj | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
5 | 3, 4 | mpbii 232 | . . 3 ⊢ (𝑥 = 𝐴 → 𝜓) |
6 | 2, 5 | exlimi 2210 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓) |
7 | 1, 6 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1539 ∃wex 1782 Ⅎwnf 1786 ∈ wcel 2106 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-12 2171 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-nf 1787 df-sb 2068 df-clab 2716 df-clel 2816 |
This theorem is referenced by: vtoclgOLD 3506 ceqsexg 3583 elabgOLD 3608 mob 3652 opeliunxp2 5747 fvopab5 6907 opeliunxp2f 8026 fprodsplit1f 15700 cnextfvval 23216 dvfsumlem2 25191 dvfsumlem4 25193 bnj981 32930 dmrelrnrel 42765 fmul01 43121 fmuldfeq 43124 fmul01lt1lem1 43125 stoweidlem3 43544 stoweidlem26 43567 stoweidlem31 43572 stoweidlem43 43584 stoweidlem51 43592 fourierdlem86 43733 fourierdlem89 43736 fourierdlem91 43738 salpreimagelt 44244 salpreimalegt 44246 |
Copyright terms: Public domain | W3C validator |