![]() |
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 3498 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | df-csb 3908 | . . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} | |
3 | sbcel2gv 3862 | . . . . . . . 8 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | |
4 | 3 | eqabcdv 2873 | . . . . . . 7 ⊢ (𝑦 ∈ V → {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} = 𝑦) |
5 | 2, 4 | eqtrid 2786 | . . . . . 6 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑥 = 𝑦) |
6 | 5 | elv 3482 | . . . . 5 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦 |
7 | 6 | csbeq2i 3915 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑦⦌𝑦 |
8 | csbcow 3922 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑥⦌𝑥 | |
9 | df-csb 3908 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌𝑦 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} | |
10 | 7, 8, 9 | 3eqtr3i 2770 | . . 3 ⊢ ⦋𝐴 / 𝑥⦌𝑥 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} |
11 | sbcel2gv 3862 | . . . 4 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) | |
12 | 11 | eqabcdv 2873 | . . 3 ⊢ (𝐴 ∈ V → {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} = 𝐴) |
13 | 10, 12 | eqtrid 2786 | . 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
14 | 1, 13 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1536 ∈ wcel 2105 {cab 2711 Vcvv 3477 [wsbc 3790 ⦋csb 3907 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-12 2174 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1539 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-v 3479 df-sbc 3791 df-csb 3908 |
This theorem is referenced by: csbvargi 4440 sbccsb2 4442 2nreu 4449 csbfv 6956 ixpsnval 8938 csbwrdg 14578 swrdspsleq 14699 prmgaplem7 17090 telgsums 20025 ixpsnbasval 21232 scmatscm 22534 pm2mpf1lem 22815 pm2mpcoe1 22821 idpm2idmp 22822 pm2mpmhmlem2 22840 monmat2matmon 22845 pm2mp 22846 fvmptnn04if 22870 chfacfscmulfsupp 22880 cayhamlem4 22909 divcncf 25495 opsbc2ie 32503 esum2dlem 34072 relowlpssretop 37346 rdgeqoa 37352 renegclALT 38944 cdlemk40 40899 tfsconcatfv 43330 iscard4 43522 minregex 43523 cotrclrcl 43731 frege124d 43750 frege70 43922 frege72 43924 frege77 43929 frege91 43943 frege92 43944 frege116 43968 frege118 43970 frege120 43972 rusbcALT 44434 onfrALTlem5 44539 onfrALTlem4 44540 onfrALTlem5VD 44882 iccelpart 47357 ply1mulgsumlem4 48234 |
Copyright terms: Public domain | W3C validator |