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 3773 | . 2 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 [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-cleq 2814 df-clel 2893 df-sbc 3772 |
This theorem is referenced by: sbceq1dd 3777 sbcnestgfw 4369 sbcnestgf 4374 ralrnmptw 6853 ralrnmpt 6855 tfindes 7565 findes 7600 findcard2 8747 ac6sfi 8751 indexfi 8821 ac6num 9890 nn1suc 11648 uzind4s 12297 uzind4s2 12298 fzrevral 12982 fzshftral 12985 fi1uzind 13845 wrdind 14074 wrd2ind 14075 cjth 14452 prmind2 16019 isprs 17530 isdrs 17534 joinlem 17611 meetlem 17625 istos 17635 isdlat 17793 gsumvalx 17876 mndind 17982 issrg 19188 islmod 19569 quotval 24810 nn0min 30464 wrdt2ind 30555 bnj944 32110 sdclem2 34900 fdc 34903 hdmap1ffval 38813 hdmap1fval 38814 rexrabdioph 39271 2nn0ind 39422 zindbi 39423 iotasbcq 40649 prproropreud 43518 |
Copyright terms: Public domain | W3C validator |