Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbceq1a | Structured version Visualization version GIF version |
Description: Equality theorem for class substitution. Class version of sbequ12 2097. (Contributed by NM, 26-Sep-2003.) |
Ref | Expression |
---|---|
sbceq1a | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbid 2100 | . 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑) | |
2 | dfsbcq2 3405 | . 2 ⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
3 | 1, 2 | syl5bbr 273 | 1 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 [wsb 1867 [wsbc 3402 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-sbc 3403 |
This theorem is referenced by: sbceq2a 3414 elrabsf 3441 cbvralcsf 3531 rabsnifsb 4201 euotd 4900 wfisg 5632 elfvmptrab1 6213 ralrnmpt 6276 riotass2 6537 riotass 6538 oprabv 6601 elovmpt2rab 6778 elovmpt2rab1 6779 ovmpt3rabdm 6790 elovmpt3rab1 6791 tfindes 6954 sbcopeq1a 7111 mpt2xopoveq 7232 findcard2 8085 ac6sfi 8089 indexfi 8157 nn0ind-raph 11353 fzrevral 12294 wrdind 13328 wrd2ind 13329 prmind2 15236 elmptrab 21440 isfildlem 21471 gropd 25708 grstructd 25709 vtocl2d 28699 ifeqeqx 28745 bnj919 30091 bnj976 30102 bnj1468 30170 bnj110 30182 bnj150 30200 bnj151 30201 bnj607 30240 bnj873 30248 bnj849 30249 bnj1388 30355 setinds 30927 dfon2lem1 30932 tfisg 30960 frinsg 30986 indexdom 32699 sdclem2 32708 sdclem1 32709 fdc1 32712 riotasv2s 33262 elimhyps 33265 sbccomieg 36375 rexrabdioph 36376 rexfrabdioph 36377 aomclem6 36647 pm13.13a 37630 pm13.13b 37631 pm13.14 37632 tratrb 37767 uzwo4 38246 |
Copyright terms: Public domain | W3C validator |