![]() |
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 2797 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝑥 = 𝐵) |
5 | sbcied2.3 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) | |
6 | 4, 5 | syldan 591 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) |
7 | 1, 6 | sbcied 3837 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∈ wcel 2106 [wsbc 3791 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-sbc 3792 |
This theorem is referenced by: iscat 17717 sectffval 17798 issubc 17886 isfunc 17915 cat1 18151 ismgm 18667 issgrp 18746 isnsg 19186 isrng 20172 isring 20255 isdomn 20722 islbs 21093 isassa 21894 opsrval 22082 isuhgr 29092 isushgr 29093 isupgr 29116 isumgr 29127 isuspgr 29184 isusgr 29185 isgrim 47806 isthinc 48821 |
Copyright terms: Public domain | W3C validator |