![]() |
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 3779 | . 2 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1540 [wsbc 3777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-cleq 2723 df-clel 2809 df-sbc 3778 |
This theorem is referenced by: sbceq1dd 3783 sbcnestgfw 4418 sbcnestgf 4423 ralrnmptw 7095 ralrnmpt 7097 tfindes 7856 findes 7897 frpoins3xpg 8131 frpoins3xp3g 8132 findcard2 9170 findcard2OLD 9290 ac6sfi 9293 indexfi 9366 ac6num 10480 nn1suc 12241 uzind4s 12899 uzind4s2 12900 fzrevral 13593 fzshftral 13596 fi1uzind 14465 wrdind 14679 wrd2ind 14680 cjth 15057 prmind2 16629 isprs 18260 isdrs 18264 joinlem 18346 meetlem 18360 istos 18381 isdlat 18485 gsumvalx 18607 mndind 18751 issrg 20089 islmod 20706 quotval 26143 nn0min 32458 wrdt2ind 32549 bnj944 34412 sdclem2 37073 fdc 37076 hdmap1ffval 41129 hdmap1fval 41130 rexrabdioph 41994 2nn0ind 42146 zindbi 42147 iotasbcq 43658 prproropreud 46635 |
Copyright terms: Public domain | W3C validator |