![]() |
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 3793 | . 2 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 = wceq 1537 [wsbc 3791 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-cleq 2727 df-clel 2814 df-sbc 3792 |
This theorem is referenced by: sbceq1dd 3797 sbcnestgfw 4427 sbcnestgf 4432 ralrnmptw 7114 ralrnmpt 7116 tfindes 7884 findes 7923 frpoins3xpg 8164 frpoins3xp3g 8165 findcard2 9203 ac6sfi 9318 indexfi 9398 ac6num 10517 nn1suc 12286 uzind4s 12948 uzind4s2 12949 fzrevral 13649 fzshftral 13652 fi1uzind 14543 wrdind 14757 wrd2ind 14758 cjth 15139 prmind2 16719 isprs 18354 isdrs 18359 joinlem 18441 meetlem 18455 istos 18476 isdlat 18580 gsumvalx 18702 mndind 18854 issrg 20206 islmod 20879 quotval 26349 nn0min 32827 wrdt2ind 32923 bnj944 34931 sdclem2 37729 fdc 37732 hdmap1ffval 41778 hdmap1fval 41779 rexrabdioph 42782 2nn0ind 42934 zindbi 42935 iotasbcq 44433 prproropreud 47434 |
Copyright terms: Public domain | W3C validator |