![]() |
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 2795 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝑥 = 𝐵) |
5 | sbcied2.3 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) | |
6 | 4, 5 | syldan 592 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) |
7 | 1, 6 | sbcied 3822 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 [wsbc 3777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-sbc 3778 |
This theorem is referenced by: iscat 17613 sectffval 17694 issubc 17782 isfunc 17811 cat1 18044 ismgm 18559 issgrp 18608 isnsg 19030 isring 20054 islbs 20680 isdomn 20903 isassa 21403 opsrval 21593 isuhgr 28310 isushgr 28311 isupgr 28334 isumgr 28345 isuspgr 28402 isusgr 28403 isrng 46637 isthinc 47595 |
Copyright terms: Public domain | W3C validator |