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 2244. (Contributed by NM, 26-Sep-2003.) |
Ref | Expression |
---|---|
sbceq1a | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbid 2248 | . 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑) | |
2 | dfsbcq2 3774 | . 2 ⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
3 | 1, 2 | syl5bbr 286 | 1 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 [wsb 2060 [wsbc 3771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-sbc 3772 |
This theorem is referenced by: sbceq2a 3783 elrabsf 3815 cbvralcsf 3924 vtocl2dOLD 3930 reusngf 4606 rexreusng 4611 reuprg0 4632 rmosn 4649 rabsnifsb 4652 euotd 5395 reuop 6138 wfisg 6177 elfvmptrab1w 6787 elfvmptrab1 6788 ralrnmpt 6855 riotass2 7133 riotass 7134 oprabv 7203 elovmporab 7380 elovmporab1w 7381 elovmporab1 7382 ovmpt3rabdm 7393 elovmpt3rab1 7394 tfindes 7565 sbcopeq1a 7739 mpoxopoveq 7876 findcard2 8747 ac6sfi 8751 indexfi 8821 nn0ind-raph 12071 fzrevral 12982 wrdind 14074 wrd2ind 14075 prmind2 16019 elmptrab 22365 isfildlem 22395 2sqreulem4 25958 gropd 26744 grstructd 26745 rspc2daf 30159 opreu2reuALT 30168 ifeqeqx 30225 wrdt2ind 30555 bnj919 31938 bnj976 31949 bnj1468 32018 bnj110 32030 bnj150 32048 bnj151 32049 bnj607 32088 bnj873 32096 bnj849 32097 bnj1388 32203 setinds 32921 dfon2lem1 32926 tfisg 32953 frpoinsg 32979 frinsg 32985 rdgssun 34542 indexdom 34892 sdclem2 34900 sdclem1 34901 fdc1 34904 riotasv2s 35976 elimhyps 35979 sbccomieg 39270 rexrabdioph 39271 rexfrabdioph 39272 aomclem6 39539 pm13.13a 40619 pm13.13b 40620 pm13.14 40621 tratrb 40750 uzwo4 41195 or2expropbilem2 43149 reuf1odnf 43187 ich2exprop 43480 ichnreuop 43481 ichreuopeq 43482 prproropreud 43518 reupr 43531 reuopreuprim 43535 |
Copyright terms: Public domain | W3C validator |