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 2728 | . . 3 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) |
4 | 1, 3 | eleq12d 2682 | . 2 ⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝐵 ∈ {𝑥 ∣ 𝜒})) |
5 | df-sbc 3403 | . 2 ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝐴 ∈ {𝑥 ∣ 𝜓}) | |
6 | df-sbc 3403 | . 2 ⊢ ([𝐵 / 𝑥]𝜒 ↔ 𝐵 ∈ {𝑥 ∣ 𝜒}) | |
7 | 4, 5, 6 | 3bitr4g 302 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 ∈ wcel 1977 {cab 2596 [wsbc 3402 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-sbc 3403 |
This theorem is referenced by: fpwwe2cbv 9331 fpwwe2lem2 9333 fpwwe2lem3 9334 fi1uzind 13134 fi1uzindOLD 13140 isprs 16753 isdrs 16757 istos 16858 isdlat 17016 issrg 18330 islmod 18690 fdc 32711 hdmap1ffval 36103 hdmap1fval 36104 hdmapffval 36136 hdmapfval 36137 hgmapffval 36195 hgmapfval 36196 sbccomieg 36375 rexrabdioph 36376 |
Copyright terms: Public domain | W3C validator |