![]() |
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 2801 | . . 3 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) |
4 | 1, 3 | eleq12d 2827 | . 2 ⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝐵 ∈ {𝑥 ∣ 𝜒})) |
5 | df-sbc 3778 | . 2 ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝐴 ∈ {𝑥 ∣ 𝜓}) | |
6 | df-sbc 3778 | . 2 ⊢ ([𝐵 / 𝑥]𝜒 ↔ 𝐵 ∈ {𝑥 ∣ 𝜒}) | |
7 | 4, 5, 6 | 3bitr4g 313 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1541 ∈ wcel 2106 {cab 2709 [wsbc 3777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-sbc 3778 |
This theorem is referenced by: sbcbidv 3836 frpoins3xpg 8128 frpoins3xp3g 8129 fpwwe2cbv 10627 fpwwe2lem2 10629 fpwwe2lem3 10630 fi1uzind 14460 isprs 18252 isdrs 18256 istos 18373 isdlat 18477 issrg 20013 islmod 20479 fdc 36699 hdmap1ffval 40752 hdmap1fval 40753 hdmapffval 40783 hdmapfval 40784 hgmapffval 40842 hgmapfval 40843 sbccomieg 41613 rexrabdioph 41614 |
Copyright terms: Public domain | W3C validator |