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 315 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∈ wcel 2105 {cab 2799 [wsbc 3771 |
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-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-sbc 3772 |
This theorem is referenced by: sbcbidv 3826 fpwwe2cbv 10041 fpwwe2lem2 10043 fpwwe2lem3 10044 fi1uzind 13845 isprs 17530 isdrs 17534 istos 17635 isdlat 17793 issrg 19188 islmod 19569 fdc 34903 hdmap1ffval 38813 hdmap1fval 38814 hdmapffval 38844 hdmapfval 38845 hgmapffval 38903 hgmapfval 38904 sbccomieg 39270 rexrabdioph 39271 |
Copyright terms: Public domain | W3C validator |