![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbceq1a | Structured version Visualization version Unicode version |
Description: Equality theorem for class substitution. Class version of sbequ12 2094. (Contributed by NM, 26-Sep-2003.) |
Ref | Expression |
---|---|
sbceq1a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbid 2097 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | dfsbcq2 3282 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl5bbr 267 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-12 1944 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-sbc 3280 |
This theorem is referenced by: sbceq2a 3291 elrabsf 3318 cbvralcsf 3407 rabsnifsb 4053 euotd 4719 wfisg 5438 elfvmptrab1 5998 ralrnmpt 6059 riotass2 6308 riotass 6309 oprabv 6371 elovmpt2rab 6547 elovmpt2rab1 6548 ovmpt3rabdm 6558 elovmpt3rab1 6559 tfindes 6721 sbcopeq1a 6877 mpt2xopoveq 6997 findcard2 7842 ac6sfi 7846 indexfi 7913 nn0ind-raph 11069 fzrevral 11914 wrdind 12876 wrd2ind 12877 prmind2 14690 elmptrab 20897 isfildlem 20927 vtocl2d 28165 ifeqeqx 28213 bnj919 29628 bnj976 29639 bnj1468 29707 bnj110 29719 bnj150 29737 bnj151 29738 bnj607 29777 bnj873 29785 bnj849 29786 bnj1388 29892 setinds 30474 dfon2lem1 30479 tfisg 30507 frinsg 30533 indexdom 32107 sdclem2 32117 sdclem1 32118 fdc1 32121 riotasv2s 32576 sbccomieg 35682 rexrabdioph 35683 rexfrabdioph 35684 aomclem6 35963 pm13.13a 36803 pm13.13b 36804 pm13.14 36805 tratrb 36942 uzwo4 37431 gropd 39275 grstructd 39276 |
Copyright terms: Public domain | W3C validator |