| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > vtoclg1f | Structured version Visualization version GIF version | ||
| Description: Version of vtoclgf 3529 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-10 2178 and ax-11 2194. (Contributed by BJ, 1-May-2019.) |
| Ref | Expression |
|---|---|
| vtoclg1f.nf | ⊢ Ⅎ𝑥𝜓 |
| vtoclg1f.maj | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| vtoclg1f.min | ⊢ 𝜑 |
| Ref | Expression |
|---|---|
| vtoclg1f | ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elisset 2842 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
| 2 | vtoclg1f.nf | . . 3 ⊢ Ⅎ𝑥𝜓 | |
| 3 | vtoclg1f.min | . . . 4 ⊢ 𝜑 | |
| 4 | vtoclg1f.maj | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 5 | 3, 4 | mpbii 236 | . . 3 ⊢ (𝑥 = 𝐴 → 𝜓) |
| 6 | 2, 5 | exlimi 2253 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓) |
| 7 | 1, 6 | syl 18 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ↔ wb 209 = wceq 1570 ∃wex 1812 Ⅎwnf 1816 ∈ wcel 2145 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-12 2213 |
| This proof depends on definitions: df-bi 210 df-an 402 df-tru 1573 df-ex 1813 df-nf 1817 df-sb 2100 df-clab 2739 df-clel 2835 |
| This theorem is used by: ceqsexg 3607 mob 3675 opeliunxp2 5812 fvopab5 7016 opeliunxp2f 8206 fprodsplit1f 16110 cnextfvval 24331 dvfsumlem2 26294 dvfsumlem4 26296 bnj981 35500 dmrelrnrel 46154 fmul01 46508 fmuldfeq 46511 fmul01lt1lem1 46512 fprodcnlem 46527 stoweidlem3 46929 stoweidlem26 46952 stoweidlem31 46957 stoweidlem43 46969 stoweidlem51 46977 fourierdlem86 47118 fourierdlem89 47121 fourierdlem91 47123 sge0f1o 47308 salpreimagelt 47633 salpreimalegt 47635 |
| Copyright terms: Public domain | W3C validator |