|   | 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 3789 | . 2 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1539 [wsbc 3787 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 df-clel 2815 df-sbc 3788 | 
| This theorem is referenced by: sbceq1dd 3793 sbcnestgfw 4420 sbcnestgf 4425 ralrnmptw 7113 ralrnmpt 7115 tfindes 7885 findes 7923 frpoins3xpg 8166 frpoins3xp3g 8167 findcard2 9205 ac6sfi 9321 indexfi 9401 ac6num 10520 nn1suc 12289 uzind4s 12951 uzind4s2 12952 fzrevral 13653 fzshftral 13656 fi1uzind 14547 wrdind 14761 wrd2ind 14762 cjth 15143 prmind2 16723 isprs 18343 isdrs 18348 joinlem 18429 meetlem 18443 istos 18464 isdlat 18568 gsumvalx 18690 mndind 18842 issrg 20186 islmod 20863 quotval 26335 nn0min 32823 wrdt2ind 32939 bnj944 34953 sdclem2 37750 fdc 37753 hdmap1ffval 41798 hdmap1fval 41799 rexrabdioph 42810 2nn0ind 42962 zindbi 42963 iotasbcq 44461 prproropreud 47501 | 
| Copyright terms: Public domain | W3C validator |