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 3416 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | df-csb 3799 | . . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} | |
3 | sbcel2gv 3754 | . . . . . . . 8 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | |
4 | 3 | abbi1dv 2868 | . . . . . . 7 ⊢ (𝑦 ∈ V → {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} = 𝑦) |
5 | 2, 4 | syl5eq 2783 | . . . . . 6 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑥 = 𝑦) |
6 | 5 | elv 3404 | . . . . 5 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦 |
7 | 6 | csbeq2i 3806 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑦⦌𝑦 |
8 | csbcow 3813 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑥⦌𝑥 | |
9 | df-csb 3799 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌𝑦 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} | |
10 | 7, 8, 9 | 3eqtr3i 2767 | . . 3 ⊢ ⦋𝐴 / 𝑥⦌𝑥 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} |
11 | sbcel2gv 3754 | . . . 4 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) | |
12 | 11 | abbi1dv 2868 | . . 3 ⊢ (𝐴 ∈ V → {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} = 𝐴) |
13 | 10, 12 | syl5eq 2783 | . 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
14 | 1, 13 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2112 {cab 2714 Vcvv 3398 [wsbc 3683 ⦋csb 3798 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-12 2177 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-nf 1792 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-v 3400 df-sbc 3684 df-csb 3799 |
This theorem is referenced by: csbvargi 4333 sbccsb2 4335 2nreu 4342 csbfv 6740 ixpsnval 8559 csbwrdg 14064 swrdspsleq 14195 prmgaplem7 16573 telgsums 19332 ixpsnbasval 20201 scmatscm 21364 pm2mpf1lem 21645 pm2mpcoe1 21651 idpm2idmp 21652 pm2mpmhmlem2 21670 monmat2matmon 21675 pm2mp 21676 fvmptnn04if 21700 chfacfscmulfsupp 21710 cayhamlem4 21739 divcncf 24298 opsbc2ie 30497 esum2dlem 31726 relowlpssretop 35221 rdgeqoa 35227 renegclALT 36663 cdlemk40 38617 iscard4 40766 cotrclrcl 40968 frege124d 40987 frege70 41159 frege72 41161 frege77 41166 frege91 41180 frege92 41181 frege116 41205 frege118 41207 frege120 41209 rusbcALT 41671 onfrALTlem5 41776 onfrALTlem4 41777 onfrALTlem5VD 42119 iccelpart 44501 ply1mulgsumlem4 45346 |
Copyright terms: Public domain | W3C validator |