![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbceq1d | Structured version Visualization version GIF version |
Description: Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by NM, 30-Jun-2018.) |
Ref | Expression |
---|---|
sbceq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
sbceq1d | ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbceq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | dfsbcq 3589 | . 2 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1631 [wsbc 3587 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 df-cleq 2764 df-clel 2767 df-sbc 3588 |
This theorem is referenced by: sbceq1dd 3593 sbcnestgf 4140 ralrnmpt 6513 tfindes 7213 findes 7247 findcard2 8360 ac6sfi 8364 indexfi 8434 ac6num 9507 nn1suc 11247 uzind4s 11955 uzind4s2 11956 fzrevral 12632 fzshftral 12635 fi1uzind 13481 wrdind 13685 wrd2ind 13686 cjth 14051 prmind2 15605 isprs 17138 isdrs 17142 joinlem 17219 meetlem 17233 istos 17243 isdlat 17401 gsumvalx 17478 mrcmndind 17574 issrg 18715 islmod 19077 quotval 24267 nn0min 29907 bnj944 31346 sdclem2 33868 fdc 33871 hdmap1ffval 37603 hdmap1fval 37604 rexrabdioph 37882 2nn0ind 38034 zindbi 38035 iotasbcq 39162 |
Copyright terms: Public domain | W3C validator |