|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > sbcied2 | Structured version Visualization version GIF version | ||
| Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.) | 
| Ref | Expression | 
|---|---|
| sbcied2.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| sbcied2.2 | ⊢ (𝜑 → 𝐴 = 𝐵) | 
| sbcied2.3 | ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) | 
| Ref | Expression | 
|---|---|
| sbcied2 | ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | sbcied2.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
| 2 | id 22 | . . . 4 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) | |
| 3 | sbcied2.2 | . . . 4 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 4 | 2, 3 | sylan9eqr 2799 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝑥 = 𝐵) | 
| 5 | sbcied2.3 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) | |
| 6 | 4, 5 | syldan 591 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) | 
| 7 | 1, 6 | sbcied 3832 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 [wsbc 3788 | 
| 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-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-sbc 3789 | 
| This theorem is referenced by: iscat 17715 sectffval 17794 issubc 17880 isfunc 17909 cat1 18142 ismgm 18654 issgrp 18733 isnsg 19173 isrng 20151 isring 20234 isdomn 20705 islbs 21075 isassa 21876 opsrval 22064 isuhgr 29077 isushgr 29078 isupgr 29101 isumgr 29112 isuspgr 29169 isusgr 29170 isgrim 47868 isthinc 49069 | 
| Copyright terms: Public domain | W3C validator |