Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > csbvarg | Structured version Visualization version Unicode version |
Description: The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
csbvarg |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3212 | . 2 | |
2 | vex 3203 | . . . . . 6 | |
3 | df-csb 3534 | . . . . . . 7 | |
4 | sbcel2gv 3496 | . . . . . . . 8 | |
5 | 4 | abbi1dv 2743 | . . . . . . 7 |
6 | 3, 5 | syl5eq 2668 | . . . . . 6 |
7 | 2, 6 | ax-mp 5 | . . . . 5 |
8 | 7 | csbeq2i 3993 | . . . 4 |
9 | csbco 3543 | . . . 4 | |
10 | df-csb 3534 | . . . 4 | |
11 | 8, 9, 10 | 3eqtr3i 2652 | . . 3 |
12 | sbcel2gv 3496 | . . . 4 | |
13 | 12 | abbi1dv 2743 | . . 3 |
14 | 11, 13 | syl5eq 2668 | . 2 |
15 | 1, 14 | syl 17 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 wcel 1990 cab 2608 cvv 3200 wsbc 3435 csb 3533 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-v 3202 df-sbc 3436 df-csb 3534 |
This theorem is referenced by: sbccsb2 4005 csbfv 6233 ixpsnval 7911 csbwrdg 13334 swrdspsleq 13449 prmgaplem7 15761 telgsums 18390 ixpsnbasval 19209 scmatscm 20319 pm2mpf1lem 20599 pm2mpcoe1 20605 idpm2idmp 20606 pm2mpmhmlem2 20624 monmat2matmon 20629 pm2mp 20630 fvmptnn04if 20654 chfacfscmulfsupp 20664 cayhamlem4 20693 divcncf 23216 iuninc 29379 f1od2 29499 esum2dlem 30154 bnj110 30928 bj-sels 32950 relowlpssretop 33212 rdgeqoa 33218 finxpreclem4 33231 csbvargi 33921 renegclALT 34249 cdlemk40 36205 brtrclfv2 38019 cotrclrcl 38034 frege124d 38053 frege70 38227 frege72 38229 frege77 38234 frege91 38248 frege92 38249 frege116 38273 frege118 38275 frege120 38277 rusbcALT 38640 onfrALTlem5 38757 onfrALTlem4 38758 onfrALTlem5VD 39121 onfrALTlem4VD 39122 iccelpart 41369 ply1mulgsumlem4 42177 |
Copyright terms: Public domain | W3C validator |