Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbceqbid | Structured version Visualization version GIF version |
Description: Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018.) |
Ref | Expression |
---|---|
sbceqbid.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
sbceqbid.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
sbceqbid | ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbceqbid.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | sbceqbid.2 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 2 | abbidv 2885 | . . 3 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) |
4 | 1, 3 | eleq12d 2907 | . 2 ⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝐵 ∈ {𝑥 ∣ 𝜒})) |
5 | df-sbc 3772 | . 2 ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝐴 ∈ {𝑥 ∣ 𝜓}) | |
6 | df-sbc 3772 | . 2 ⊢ ([𝐵 / 𝑥]𝜒 ↔ 𝐵 ∈ {𝑥 ∣ 𝜒}) | |
7 | 4, 5, 6 | 3bitr4g 316 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1533 ∈ wcel 2110 {cab 2799 [wsbc 3771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1777 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-sbc 3772 |
This theorem is referenced by: sbcbidv 3826 fpwwe2cbv 10046 fpwwe2lem2 10048 fpwwe2lem3 10049 fi1uzind 13849 isprs 17534 isdrs 17538 istos 17639 isdlat 17797 issrg 19251 islmod 19632 fdc 35014 hdmap1ffval 38925 hdmap1fval 38926 hdmapffval 38956 hdmapfval 38957 hgmapffval 39015 hgmapfval 39016 sbccomieg 39383 rexrabdioph 39384 |
Copyright terms: Public domain | W3C validator |