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 3713 | . 2 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1539 [wsbc 3711 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1784 df-cleq 2730 df-clel 2817 df-sbc 3712 |
This theorem is referenced by: sbceq1dd 3717 sbcnestgfw 4349 sbcnestgf 4354 ralrnmptw 6952 ralrnmpt 6954 tfindes 7684 findes 7723 findcard2 8909 findcard2OLD 8986 ac6sfi 8988 indexfi 9057 ac6num 10166 nn1suc 11925 uzind4s 12577 uzind4s2 12578 fzrevral 13270 fzshftral 13273 fi1uzind 14139 wrdind 14363 wrd2ind 14364 cjth 14742 prmind2 16318 isprs 17930 isdrs 17934 joinlem 18016 meetlem 18030 istos 18051 isdlat 18155 gsumvalx 18275 mndind 18381 issrg 19658 islmod 20042 quotval 25357 nn0min 31036 wrdt2ind 31127 bnj944 32818 frpoins3xpg 33714 frpoins3xp3g 33715 sdclem2 35827 fdc 35830 hdmap1ffval 39736 hdmap1fval 39737 rexrabdioph 40532 2nn0ind 40683 zindbi 40684 iotasbcq 41944 prproropreud 44849 |
Copyright terms: Public domain | W3C validator |