![]() |
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 2129, ax-12 2166. (Revised by GG, 12-Oct-2024.) |
Ref | Expression |
---|---|
sbcied.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
sbcied.2 | ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
sbcied | ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sbc 3774 | . 2 ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝐴 ∈ {𝑥 ∣ 𝜓}) | |
2 | sbcied.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
3 | sbcied.2 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | elabd3 3656 | . 2 ⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜒)) |
5 | 1, 4 | bitrid 282 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1533 ∈ wcel 2098 {cab 2702 [wsbc 3773 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-sbc 3774 |
This theorem is referenced by: sbcied2 3821 sbc2ie 3856 sbc2iedv 3858 sbc3ie 3859 sbcralt 3862 csbied 3927 euotd 5515 fmptsnd 7178 riota5f 7404 fpwwe2lem11 10666 fpwwe2lem12 10667 brfi1uzind 14495 opfi1uzind 14498 sbcie3s 17134 issubc 17824 gsumvalx 18639 dmdprd 19967 dprdval 19972 issrg 20140 issrng 20742 islmhm 20924 isphl 21577 istmd 24022 istgp 24025 isnlm 24636 isclm 25035 iscph 25142 iscms 25317 limcfval 25845 ewlksfval 29487 sbcies 32364 abfmpeld 32521 abfmpel 32522 isomnd 32871 isorng 33113 rprmval 33328 f1o2d2 41857 |
Copyright terms: Public domain | W3C validator |