Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > abid | Structured version Visualization version GIF version |
Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
abid | ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-clab 2597 | . 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑) | |
2 | sbid 2100 | . 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑) | |
3 | 1, 2 | bitri 263 | 1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 [wsb 1867 ∈ wcel 1977 {cab 2596 |
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-12 2034 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-sb 1868 df-clab 2597 |
This theorem is referenced by: abeq2 2719 abeq2d 2721 abbi 2724 abid2f 2777 abeq2f 2778 elabgt 3316 elabgf 3317 ralab2 3338 rexab2 3340 ss2ab 3633 ab0 3905 abn0 3908 sbccsb 3956 sbccsb2 3957 tpid3gOLD 4249 eluniab 4383 elintab 4422 iunab 4502 iinab 4517 zfrep4 4707 sniota 5795 opabiota 6171 eusvobj2 6542 eloprabga 6645 finds2 6986 wfrlem12 7313 en3lplem2 8395 scottexs 8633 scott0s 8634 cp 8637 cardprclem 8688 cfflb 8964 fin23lem29 9046 axdc3lem2 9156 4sqlem12 15498 xkococn 21273 ptcmplem4 21669 ofpreima 28848 qqhval2 29354 esum2dlem 29481 sigaclcu2 29510 bnj1143 30115 bnj1366 30154 bnj906 30254 bnj1256 30337 bnj1259 30338 bnj1311 30346 mclsax 30720 ellines 31429 bj-abeq2 31961 bj-csbsnlem 32090 bj-sspwpwab 32239 topdifinffinlem 32371 finxpreclem6 32409 finxpnom 32414 setindtrs 36610 rababg 36898 compab 37666 tpid3gVD 38099 en3lplem2VD 38101 iunmapsn 38404 ssfiunibd 38464 setrec2lem2 42240 |
Copyright terms: Public domain | W3C validator |