![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vtoclg1f | Structured version Visualization version GIF version |
Description: Version of vtoclgf 3552 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-10 2129 and ax-11 2146. (Contributed by BJ, 1-May-2019.) |
Ref | Expression |
---|---|
vtoclg1f.nf | ⊢ Ⅎ𝑥𝜓 |
vtoclg1f.maj | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtoclg1f.min | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtoclg1f | ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisset 2809 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
2 | vtoclg1f.nf | . . 3 ⊢ Ⅎ𝑥𝜓 | |
3 | vtoclg1f.min | . . . 4 ⊢ 𝜑 | |
4 | vtoclg1f.maj | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
5 | 3, 4 | mpbii 232 | . . 3 ⊢ (𝑥 = 𝐴 → 𝜓) |
6 | 2, 5 | exlimi 2202 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓) |
7 | 1, 6 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 ∃wex 1773 Ⅎwnf 1777 ∈ wcel 2098 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-12 2163 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1536 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2704 df-clel 2804 |
This theorem is referenced by: ceqsexg 3636 elabgOLD 3662 mob 3708 opeliunxp2 5832 fvopab5 7024 opeliunxp2f 8196 fprodsplit1f 15940 cnextfvval 23924 dvfsumlem2 25916 dvfsumlem2OLD 25917 dvfsumlem4 25919 bnj981 34490 dmrelrnrel 44494 fmul01 44865 fmuldfeq 44868 fmul01lt1lem1 44869 fprodcnlem 44884 stoweidlem3 45288 stoweidlem26 45311 stoweidlem31 45316 stoweidlem43 45328 stoweidlem51 45336 fourierdlem86 45477 fourierdlem89 45480 fourierdlem91 45482 salpreimagelt 45992 salpreimalegt 45994 |
Copyright terms: Public domain | W3C validator |