Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > csbvarg | Structured version Visualization version GIF 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 3510 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | df-csb 3881 | . . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} | |
3 | sbcel2gv 3838 | . . . . . . . 8 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | |
4 | 3 | abbi1dv 2949 | . . . . . . 7 ⊢ (𝑦 ∈ V → {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} = 𝑦) |
5 | 2, 4 | syl5eq 2865 | . . . . . 6 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑥 = 𝑦) |
6 | 5 | elv 3497 | . . . . 5 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦 |
7 | 6 | csbeq2i 3888 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑦⦌𝑦 |
8 | csbcow 3895 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑥⦌𝑥 | |
9 | df-csb 3881 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌𝑦 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} | |
10 | 7, 8, 9 | 3eqtr3i 2849 | . . 3 ⊢ ⦋𝐴 / 𝑥⦌𝑥 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} |
11 | sbcel2gv 3838 | . . . 4 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) | |
12 | 11 | abbi1dv 2949 | . . 3 ⊢ (𝐴 ∈ V → {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} = 𝐴) |
13 | 10, 12 | syl5eq 2865 | . 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
14 | 1, 13 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 {cab 2796 Vcvv 3492 [wsbc 3769 ⦋csb 3880 |
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 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-v 3494 df-sbc 3770 df-csb 3881 |
This theorem is referenced by: csbvargi 4381 sbccsb2 4383 2nreu 4389 csbfv 6708 ixpsnval 8452 csbwrdg 13883 swrdspsleq 14015 prmgaplem7 16381 telgsums 19042 ixpsnbasval 19910 scmatscm 21050 pm2mpf1lem 21330 pm2mpcoe1 21336 idpm2idmp 21337 pm2mpmhmlem2 21355 monmat2matmon 21360 pm2mp 21361 fvmptnn04if 21385 chfacfscmulfsupp 21395 cayhamlem4 21424 divcncf 23975 opsbc2ie 30166 esum2dlem 31250 relowlpssretop 34527 rdgeqoa 34533 renegclALT 35979 cdlemk40 37933 iscard4 39778 cotrclrcl 39965 frege124d 39984 frege70 40157 frege72 40159 frege77 40164 frege91 40178 frege92 40179 frege116 40203 frege118 40205 frege120 40207 rusbcALT 40648 onfrALTlem5 40753 onfrALTlem4 40754 onfrALTlem5VD 41096 iccelpart 43470 ply1mulgsumlem4 44371 |
Copyright terms: Public domain | W3C validator |