![]() |
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 3708 | . 2 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1522 [wsbc 3706 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1762 df-cleq 2788 df-clel 2863 df-sbc 3707 |
This theorem is referenced by: sbceq1dd 3712 sbcnestgf 4290 ralrnmpt 6725 tfindes 7433 findes 7468 findcard2 8604 ac6sfi 8608 indexfi 8678 ac6num 9747 nn1suc 11507 uzind4s 12157 uzind4s2 12158 fzrevral 12842 fzshftral 12845 fi1uzind 13701 wrdind 13920 wrd2ind 13921 cjth 14296 prmind2 15858 isprs 17369 isdrs 17373 joinlem 17450 meetlem 17464 istos 17474 isdlat 17632 gsumvalx 17709 mndind 17805 issrg 18947 islmod 19328 quotval 24564 nn0min 30221 wrdt2ind 30306 bnj944 31826 sdclem2 34549 fdc 34552 hdmap1ffval 38462 hdmap1fval 38463 rexrabdioph 38876 2nn0ind 39027 zindbi 39028 iotasbcq 40307 prproropreud 43153 |
Copyright terms: Public domain | W3C validator |