![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vtoclg1f | Structured version Visualization version GIF version |
Description: Version of vtoclgf 3555 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 2810 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
2 | vtoclg1f.nf | . . 3 ⊢ Ⅎ𝑥𝜓 | |
3 | vtoclg1f.min | . . . 4 ⊢ 𝜑 | |
4 | vtoclg1f.maj | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
5 | 3, 4 | mpbii 232 | . . 3 ⊢ (𝑥 = 𝐴 → 𝜓) |
6 | 2, 5 | exlimi 2205 | . 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 2166 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2705 df-clel 2805 |
This theorem is referenced by: ceqsexg 3639 elabgOLD 3666 mob 3712 opeliunxp2 5843 fvopab5 7041 opeliunxp2f 8220 fprodsplit1f 15972 cnextfvval 23987 dvfsumlem2 25979 dvfsumlem2OLD 25980 dvfsumlem4 25982 bnj981 34586 dmrelrnrel 44602 fmul01 44970 fmuldfeq 44973 fmul01lt1lem1 44974 fprodcnlem 44989 stoweidlem3 45393 stoweidlem26 45416 stoweidlem31 45421 stoweidlem43 45433 stoweidlem51 45441 fourierdlem86 45582 fourierdlem89 45585 fourierdlem91 45587 salpreimagelt 46097 salpreimalegt 46099 |
Copyright terms: Public domain | W3C validator |