![]() |
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 1957 | . 2 ⊢ Ⅎ𝑥𝜑 | |
4 | nfvd 1958 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
5 | 1, 2, 3, 4 | sbciedf 3688 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1601 ∈ wcel 2107 [wsbc 3652 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-v 3400 df-sbc 3653 |
This theorem is referenced by: sbcied2 3690 sbc2iedv 3724 sbc3ie 3725 sbcralt 3728 euotd 5210 fmptsnd 6702 riota5f 6908 fpwwe2lem12 9798 fpwwe2lem13 9799 brfi1uzind 13594 opfi1uzind 13597 sbcie3s 16313 issubc 16880 gsumvalx 17656 dmdprd 18784 dprdval 18789 issrg 18894 issrng 19242 islmhm 19422 isassa 19712 isphl 20371 istmd 22286 istgp 22289 isnlm 22887 isclm 23271 iscph 23377 iscms 23551 limcfval 24073 ewlksfval 26949 sbcies 29894 abfmpeld 30019 abfmpel 30020 isomnd 30263 isorng 30361 |
Copyright terms: Public domain | W3C validator |