![]() |
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 3492 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | df-csb 3895 | . . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} | |
3 | sbcel2gv 3850 | . . . . . . . 8 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | |
4 | 3 | eqabcdv 2864 | . . . . . . 7 ⊢ (𝑦 ∈ V → {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} = 𝑦) |
5 | 2, 4 | eqtrid 2780 | . . . . . 6 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑥 = 𝑦) |
6 | 5 | elv 3479 | . . . . 5 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦 |
7 | 6 | csbeq2i 3902 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑦⦌𝑦 |
8 | csbcow 3909 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑥⦌𝑥 | |
9 | df-csb 3895 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌𝑦 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} | |
10 | 7, 8, 9 | 3eqtr3i 2764 | . . 3 ⊢ ⦋𝐴 / 𝑥⦌𝑥 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} |
11 | sbcel2gv 3850 | . . . 4 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) | |
12 | 11 | eqabcdv 2864 | . . 3 ⊢ (𝐴 ∈ V → {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} = 𝐴) |
13 | 10, 12 | eqtrid 2780 | . 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
14 | 1, 13 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 {cab 2705 Vcvv 3473 [wsbc 3778 ⦋csb 3894 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-12 2166 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3475 df-sbc 3779 df-csb 3895 |
This theorem is referenced by: csbvargi 4436 sbccsb2 4438 2nreu 4445 csbfv 6952 ixpsnval 8925 csbwrdg 14534 swrdspsleq 14655 prmgaplem7 17033 telgsums 19955 ixpsnbasval 21108 scmatscm 22435 pm2mpf1lem 22716 pm2mpcoe1 22722 idpm2idmp 22723 pm2mpmhmlem2 22741 monmat2matmon 22746 pm2mp 22747 fvmptnn04if 22771 chfacfscmulfsupp 22781 cayhamlem4 22810 divcncf 25396 opsbc2ie 32295 esum2dlem 33744 relowlpssretop 36876 rdgeqoa 36882 renegclALT 38467 cdlemk40 40422 tfsconcatfv 42801 iscard4 42994 minregex 42995 cotrclrcl 43203 frege124d 43222 frege70 43394 frege72 43396 frege77 43401 frege91 43415 frege92 43416 frege116 43440 frege118 43442 frege120 43444 rusbcALT 43907 onfrALTlem5 44012 onfrALTlem4 44013 onfrALTlem5VD 44355 iccelpart 46802 ply1mulgsumlem4 47535 |
Copyright terms: Public domain | W3C validator |