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 3512 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | df-csb 3883 | . . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} | |
3 | sbcel2gv 3840 | . . . . . . . 8 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | |
4 | 3 | abbi1dv 2952 | . . . . . . 7 ⊢ (𝑦 ∈ V → {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} = 𝑦) |
5 | 2, 4 | syl5eq 2868 | . . . . . 6 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑥 = 𝑦) |
6 | 5 | elv 3499 | . . . . 5 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦 |
7 | 6 | csbeq2i 3890 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑦⦌𝑦 |
8 | csbcow 3897 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑥⦌𝑥 | |
9 | df-csb 3883 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌𝑦 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} | |
10 | 7, 8, 9 | 3eqtr3i 2852 | . . 3 ⊢ ⦋𝐴 / 𝑥⦌𝑥 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} |
11 | sbcel2gv 3840 | . . . 4 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) | |
12 | 11 | abbi1dv 2952 | . . 3 ⊢ (𝐴 ∈ V → {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} = 𝐴) |
13 | 10, 12 | syl5eq 2868 | . 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
14 | 1, 13 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2110 {cab 2799 Vcvv 3494 [wsbc 3771 ⦋csb 3882 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-v 3496 df-sbc 3772 df-csb 3883 |
This theorem is referenced by: csbvargi 4383 sbccsb2 4385 2nreu 4392 csbfv 6709 ixpsnval 8458 csbwrdg 13889 swrdspsleq 14021 prmgaplem7 16387 telgsums 19107 ixpsnbasval 19976 scmatscm 21116 pm2mpf1lem 21396 pm2mpcoe1 21402 idpm2idmp 21403 pm2mpmhmlem2 21421 monmat2matmon 21426 pm2mp 21427 fvmptnn04if 21451 chfacfscmulfsupp 21461 cayhamlem4 21490 divcncf 24042 opsbc2ie 30233 esum2dlem 31346 relowlpssretop 34639 rdgeqoa 34645 renegclALT 36093 cdlemk40 38047 iscard4 39893 cotrclrcl 40080 frege124d 40099 frege70 40272 frege72 40274 frege77 40279 frege91 40293 frege92 40294 frege116 40318 frege118 40320 frege120 40322 rusbcALT 40764 onfrALTlem5 40869 onfrALTlem4 40870 onfrALTlem5VD 41212 iccelpart 43587 ply1mulgsumlem4 44437 |
Copyright terms: Public domain | W3C validator |