![]() |
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 3586 | . 2 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1629 [wsbc 3584 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1868 ax-4 1883 ax-5 1989 ax-6 2055 ax-7 2091 ax-9 2152 ax-ext 2749 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1851 df-cleq 2762 df-clel 2765 df-sbc 3585 |
This theorem is referenced by: sbceq1dd 3590 sbcnestgf 4136 ralrnmpt 6510 tfindes 7207 findes 7241 findcard2 8354 ac6sfi 8358 indexfi 8428 ac6num 9501 nn1suc 11241 uzind4s 11949 uzind4s2 11950 fzrevral 12631 fzshftral 12634 fi1uzind 13484 wrdind 13688 wrd2ind 13689 cjth 14054 prmind2 15611 isprs 17144 isdrs 17148 joinlem 17225 meetlem 17239 istos 17249 isdlat 17407 gsumvalx 17484 mrcmndind 17580 issrg 18721 islmod 19083 quotval 24273 nn0min 29908 bnj944 31347 sdclem2 33870 fdc 33873 hdmap1ffval 37605 hdmap1fval 37606 rexrabdioph 37884 2nn0ind 38036 zindbi 38037 iotasbcq 39164 |
Copyright terms: Public domain | W3C validator |