| 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 3501 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
| 2 | df-csb 3900 | . . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} | |
| 3 | sbcel2gv 3857 | . . . . . . . 8 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | |
| 4 | 3 | eqabcdv 2876 | . . . . . . 7 ⊢ (𝑦 ∈ V → {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} = 𝑦) |
| 5 | 2, 4 | eqtrid 2789 | . . . . . 6 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑥 = 𝑦) |
| 6 | 5 | elv 3485 | . . . . 5 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦 |
| 7 | 6 | csbeq2i 3907 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑦⦌𝑦 |
| 8 | csbcow 3914 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑥⦌𝑥 | |
| 9 | df-csb 3900 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌𝑦 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} | |
| 10 | 7, 8, 9 | 3eqtr3i 2773 | . . 3 ⊢ ⦋𝐴 / 𝑥⦌𝑥 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} |
| 11 | sbcel2gv 3857 | . . . 4 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) | |
| 12 | 11 | eqabcdv 2876 | . . 3 ⊢ (𝐴 ∈ V → {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} = 𝐴) |
| 13 | 10, 12 | eqtrid 2789 | . 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
| 14 | 1, 13 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 {cab 2714 Vcvv 3480 [wsbc 3788 ⦋csb 3899 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-sbc 3789 df-csb 3900 |
| This theorem is referenced by: csbvargi 4435 sbccsb2 4437 2nreu 4444 csbfv 6956 ixpsnval 8940 csbwrdg 14582 swrdspsleq 14703 prmgaplem7 17095 telgsums 20011 ixpsnbasval 21215 scmatscm 22519 pm2mpf1lem 22800 pm2mpcoe1 22806 idpm2idmp 22807 pm2mpmhmlem2 22825 monmat2matmon 22830 pm2mp 22831 fvmptnn04if 22855 chfacfscmulfsupp 22865 cayhamlem4 22894 divcncf 25482 opsbc2ie 32495 esum2dlem 34093 relowlpssretop 37365 rdgeqoa 37371 renegclALT 38964 cdlemk40 40919 tfsconcatfv 43354 iscard4 43546 minregex 43547 cotrclrcl 43755 frege124d 43774 frege70 43946 frege72 43948 frege77 43953 frege91 43967 frege92 43968 frege116 43992 frege118 43994 frege120 43996 rusbcALT 44458 onfrALTlem5 44562 onfrALTlem4 44563 onfrALTlem5VD 44905 iccelpart 47420 ply1mulgsumlem4 48306 |
| Copyright terms: Public domain | W3C validator |