|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > vtoclgf | Structured version Visualization version GIF version | ||
| Description: Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro, 10-Oct-2016.) | 
| Ref | Expression | 
|---|---|
| vtoclgf.1 | ⊢ Ⅎ𝑥𝐴 | 
| vtoclgf.2 | ⊢ Ⅎ𝑥𝜓 | 
| vtoclgf.3 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | 
| vtoclgf.4 | ⊢ 𝜑 | 
| Ref | Expression | 
|---|---|
| vtoclgf | ⊢ (𝐴 ∈ 𝑉 → 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | elex 3501 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
| 2 | vtoclgf.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
| 3 | 2 | issetf 3497 | . . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | 
| 4 | vtoclgf.2 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
| 5 | vtoclgf.4 | . . . . 5 ⊢ 𝜑 | |
| 6 | vtoclgf.3 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 7 | 5, 6 | mpbii 233 | . . . 4 ⊢ (𝑥 = 𝐴 → 𝜓) | 
| 8 | 4, 7 | exlimi 2217 | . . 3 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓) | 
| 9 | 3, 8 | sylbi 217 | . 2 ⊢ (𝐴 ∈ V → 𝜓) | 
| 10 | 1, 9 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∃wex 1779 Ⅎwnf 1783 ∈ wcel 2108 Ⅎwnfc 2890 Vcvv 3480 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-v 3482 | 
| This theorem is referenced by: vtocl2gf 3572 vtocl3gf 3573 vtoclgaf 3576 elabgf 3674 fsumsplit1 15781 ssiun2sf 32572 subtr 36315 subtr2 36316 supxrgere 45344 supxrgelem 45348 supxrge 45349 fmuldfeqlem1 45597 climsuse 45623 dvnmptdivc 45953 dvmptfprodlem 45959 stoweidlem59 46074 fourierdlem31 46153 sge0fodjrnlem 46431 | 
| Copyright terms: Public domain | W3C validator |