Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbcied | 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 |
---|---|
sbcied.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
sbcied.2 | ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
sbcied | ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcied.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
2 | sbcied.2 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | nfv 1906 | . 2 ⊢ Ⅎ𝑥𝜑 | |
4 | nfvd 1907 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
5 | 1, 2, 3, 4 | sbciedf 3810 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 ∈ wcel 2105 [wsbc 3769 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-v 3494 df-sbc 3770 |
This theorem is referenced by: sbcied2 3812 sbc2iedv 3848 sbc3ie 3849 sbcralt 3852 euotd 5394 fmptsnd 6923 riota5f 7131 fpwwe2lem12 10051 fpwwe2lem13 10052 brfi1uzind 13844 opfi1uzind 13847 sbcie3s 16529 issubc 17093 gsumvalx 17874 dmdprd 19049 dprdval 19054 issrg 19186 issrng 19550 islmhm 19728 isassa 20016 isphl 20700 istmd 22610 istgp 22613 isnlm 23211 isclm 23595 iscph 23701 iscms 23875 limcfval 24397 ewlksfval 27310 sbcies 30178 abfmpeld 30327 abfmpel 30328 isomnd 30629 isorng 30799 |
Copyright terms: Public domain | W3C validator |