| 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.) Avoid ax-10 2141, ax-12 2177. (Revised by GG, 12-Oct-2024.) |
| Ref | Expression |
|---|---|
| sbcied.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| sbcied.2 | ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| sbcied | ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-sbc 3789 | . 2 ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝐴 ∈ {𝑥 ∣ 𝜓}) | |
| 2 | sbcied.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
| 3 | sbcied.2 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) | |
| 4 | 2, 3 | elabd3 3671 | . 2 ⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜒)) |
| 5 | 1, 4 | bitrid 283 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 {cab 2714 [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: sbcied2 3833 sbc2ie 3866 sbc2iedv 3867 sbc3ie 3868 sbcralt 3872 csbied 3935 euotd 5518 fmptsnd 7189 riota5f 7416 fpwwe2lem11 10681 fpwwe2lem12 10682 brfi1uzind 14547 opfi1uzind 14550 sbcie3s 17199 issubc 17880 gsumvalx 18689 dmdprd 20018 dprdval 20023 issrg 20185 issrng 20845 islmhm 21026 isphl 21646 istmd 24082 istgp 24085 isnlm 24696 isclm 25097 iscph 25204 iscms 25379 limcfval 25907 ewlksfval 29619 sbcies 32507 abfmpeld 32664 abfmpel 32665 isomnd 33078 isorng 33329 rprmval 33544 f1o2d2 42274 |
| Copyright terms: Public domain | W3C validator |