|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > vtoclg1f | Structured version Visualization version GIF version | ||
| Description: Version of vtoclgf 3568 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-10 2140 and ax-11 2156. (Contributed by BJ, 1-May-2019.) | 
| Ref | Expression | 
|---|---|
| vtoclg1f.nf | ⊢ Ⅎ𝑥𝜓 | 
| vtoclg1f.maj | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | 
| vtoclg1f.min | ⊢ 𝜑 | 
| Ref | Expression | 
|---|---|
| vtoclg1f | ⊢ (𝐴 ∈ 𝑉 → 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | elisset 2822 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
| 2 | vtoclg1f.nf | . . 3 ⊢ Ⅎ𝑥𝜓 | |
| 3 | vtoclg1f.min | . . . 4 ⊢ 𝜑 | |
| 4 | vtoclg1f.maj | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 5 | 3, 4 | mpbii 233 | . . 3 ⊢ (𝑥 = 𝐴 → 𝜓) | 
| 6 | 2, 5 | exlimi 2216 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓) | 
| 7 | 1, 6 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1539 ∃wex 1778 Ⅎwnf 1782 ∈ wcel 2107 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-nf 1783 df-sb 2064 df-clab 2714 df-clel 2815 | 
| This theorem is referenced by: ceqsexg 3652 mob 3722 opeliunxp2 5848 fvopab5 7048 opeliunxp2f 8236 fprodsplit1f 16027 cnextfvval 24074 dvfsumlem2 26068 dvfsumlem2OLD 26069 dvfsumlem4 26071 bnj981 34965 dmrelrnrel 45236 fmul01 45600 fmuldfeq 45603 fmul01lt1lem1 45604 fprodcnlem 45619 stoweidlem3 46023 stoweidlem26 46046 stoweidlem31 46051 stoweidlem43 46063 stoweidlem51 46071 fourierdlem86 46212 fourierdlem89 46215 fourierdlem91 46217 sge0f1o 46402 salpreimagelt 46727 salpreimalegt 46729 | 
| Copyright terms: Public domain | W3C validator |