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 3185 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | vex 3176 | . . . . . 6 ⊢ 𝑦 ∈ V | |
3 | df-csb 3500 | . . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} | |
4 | sbcel2gv 3463 | . . . . . . . 8 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | |
5 | 4 | abbi1dv 2730 | . . . . . . 7 ⊢ (𝑦 ∈ V → {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝑥} = 𝑦) |
6 | 3, 5 | syl5eq 2656 | . . . . . 6 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑥 = 𝑦) |
7 | 2, 6 | ax-mp 5 | . . . . 5 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦 |
8 | 7 | csbeq2i 3945 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑦⦌𝑦 |
9 | csbco 3509 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝑥 = ⦋𝐴 / 𝑥⦌𝑥 | |
10 | df-csb 3500 | . . . 4 ⊢ ⦋𝐴 / 𝑦⦌𝑦 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} | |
11 | 8, 9, 10 | 3eqtr3i 2640 | . . 3 ⊢ ⦋𝐴 / 𝑥⦌𝑥 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} |
12 | sbcel2gv 3463 | . . . 4 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑦]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) | |
13 | 12 | abbi1dv 2730 | . . 3 ⊢ (𝐴 ∈ V → {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝑦} = 𝐴) |
14 | 11, 13 | syl5eq 2656 | . 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
15 | 1, 14 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 {cab 2596 Vcvv 3173 [wsbc 3402 ⦋csb 3499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-v 3175 df-sbc 3403 df-csb 3500 |
This theorem is referenced by: sbccsb2 3957 csbfv 6143 ixpsnval 7797 csbwrdg 13189 swrdspsleq 13301 prmgaplem7 15599 telgsums 18213 ixpsnbasval 19030 scmatscm 20138 pm2mpf1lem 20418 pm2mpcoe1 20424 idpm2idmp 20425 pm2mpmhmlem2 20443 monmat2matmon 20448 pm2mp 20449 fvmptnn04if 20473 chfacfscmulfsupp 20483 cayhamlem4 20512 nbgraopALT 25953 rusgrasn 26472 iuninc 28761 f1od2 28887 esum2dlem 29481 bnj110 30182 bj-sels 32143 relowlpssretop 32388 rdgeqoa 32394 finxpreclem4 32407 csbvargi 33091 renegclALT 33267 cdlemk40 35223 brtrclfv2 37038 cotrclrcl 37053 frege124d 37072 frege70 37247 frege72 37249 frege77 37254 frege91 37268 frege92 37269 frege116 37293 frege118 37295 frege120 37297 rusbcALT 37662 onfrALTlem5 37778 onfrALTlem4 37779 onfrALTlem5VD 38143 onfrALTlem4VD 38144 divcncf 38769 iccelpart 39971 ply1mulgsumlem4 41971 |
Copyright terms: Public domain | W3C validator |