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 2797 | . 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑) | |
2 | sbid 2247 | . 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑) | |
3 | 1, 2 | bitri 276 | 1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 [wsb 2060 ∈ wcel 2105 {cab 2796 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 |
This theorem is referenced by: abeq2 2942 abeq2d 2944 abbiOLD 2952 abid2f 3009 abeq2f 3010 abeq2fOLD 3011 elabgt 3660 elabgf 3661 elabg 3663 ralab2 3685 ralab2OLD 3686 rexab2 3688 rexab2OLD 3689 ss2ab 4036 ab0 4330 abn0 4333 sbccsb 4382 sbccsb2 4383 eluniab 4841 elintab 4878 iunab 4966 iinab 4981 zfrep4 5191 rnep 5790 sniota 6339 opabiota 6739 eusvobj2 7138 eloprabga 7250 finds2 7599 wfrlem12 7955 en3lplem2 9064 scottexs 9304 scott0s 9305 cp 9308 cardprclem 9396 cfflb 9669 fin23lem29 9751 axdc3lem2 9861 4sqlem12 16280 xkococn 22196 ptcmplem4 22591 ofpreima 30338 qqhval2 31122 esum2dlem 31250 sigaclcu2 31278 bnj1143 31961 bnj1366 32000 bnj906 32101 bnj1256 32184 bnj1259 32185 bnj1311 32193 mclsax 32713 frrlem10 33029 ellines 33510 bj-csbsnlem 34117 bj-reabeq 34236 topdifinffinlem 34510 rdgssun 34541 finxpreclem6 34559 finxpnom 34564 ralssiun 34570 setindtrs 39500 rababg 39811 scottabf 40453 compab 40651 tpid3gVD 41053 en3lplem2VD 41055 iunmapsn 41356 ssfiunibd 41452 absnsb 43139 symgsubmefmndALT 43996 setrec2lem2 44725 |
Copyright terms: Public domain | W3C validator |