| Intuitionistic Logic Explorer | 
      
      
      < Previous  
      Next >
      
       Nearby theorems  | 
  ||
| Mirrors > Home > ILE Home > Th. List > vtoclef | GIF version | ||
| Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 18-Aug-1993.) | 
| Ref | Expression | 
|---|---|
| vtoclef.1 | ⊢ Ⅎ𝑥𝜑 | 
| vtoclef.2 | ⊢ 𝐴 ∈ V | 
| vtoclef.3 | ⊢ (𝑥 = 𝐴 → 𝜑) | 
| Ref | Expression | 
|---|---|
| vtoclef | ⊢ 𝜑 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | vtoclef.2 | . . 3 ⊢ 𝐴 ∈ V | |
| 2 | 1 | isseti 2771 | . 2 ⊢ ∃𝑥 𝑥 = 𝐴 | 
| 3 | vtoclef.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
| 4 | vtoclef.3 | . . 3 ⊢ (𝑥 = 𝐴 → 𝜑) | |
| 5 | 3, 4 | exlimi 1608 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜑) | 
| 6 | 2, 5 | ax-mp 5 | 1 ⊢ 𝜑 | 
| Colors of variables: wff set class | 
| Syntax hints: → wi 4 = wceq 1364 Ⅎwnf 1474 ∃wex 1506 ∈ wcel 2167 Vcvv 2763 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1461 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-ext 2178 | 
| This theorem depends on definitions: df-bi 117 df-nf 1475 df-sb 1777 df-clab 2183 df-cleq 2189 df-clel 2192 df-v 2765 | 
| This theorem is referenced by: nn0ind-raph 9443 | 
| Copyright terms: Public domain | W3C validator |