| 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 2744 | . 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑) | |
| 2 | sbid 2293 | . 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑) | |
| 3 | 1, 2 | bitri 278 | 1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 209 [wsb 2093 ∈ wcel 2145 {cab 2743 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-12 2215 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-ex 1803 df-sb 2094 df-clab 2744 |
| This theorem is referenced by: eqabrd 2906 eqabf 2956 abid2fOLD 2958 elabgf 3636 ralab2 3663 rexab2 3665 ss2ab 4017 ab0ALT 4337 sbccsb 4393 sbccsb2 4394 eluniab 4882 iunab 5012 iinab 5028 zfrep4 5248 rnep 5908 sniota 6516 opabiota 6953 eusvobj2 7392 eloprabga 7509 finds2 7883 frrlem10 8280 en3lplem2 9570 scottexs 9849 scott0s 9850 scottabf 9854 cp 9865 cardprclem 9953 cfflb 10231 fin23lem29 10313 axdc3lem2 10423 4sqlem12 17006 xkococn 23778 ptcmplem4 24173 noinfbnd1lem1 27845 ofpreima 32922 algextdeglem6 34029 qqhval2 34289 esum2dlem 34399 sigaclcu2 34427 bnj1143 35095 bnj1366 35134 bnj906 35235 bnj1256 35320 bnj1259 35321 bnj1311 35329 mclsax 35932 ellines 36515 bj-csbsnlem 37400 bj-reabeq 37524 bj-velpwALT 37550 topdifinffinlem 37853 rdgssun 37884 finxpreclem6 37902 finxpnom 37907 ralssiun 37913 setindtrs 43614 rababg 44162 compab 45015 tpid3gVD 45415 en3lplem2VD 45417 permaxrep 45580 iunmapsn 45791 ssfiunibd 45886 absnsb 47619 setrec2lem2 50323 |
| Copyright terms: Public domain | W3C validator |