![]() |
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 2739 | . 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑) | |
2 | sbid 2253 | . 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑) | |
3 | 1, 2 | bitri 264 | 1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 [wsb 2038 ∈ wcel 2131 {cab 2738 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-12 2188 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1846 df-sb 2039 df-clab 2739 |
This theorem is referenced by: abeq2 2862 abeq2d 2864 abbi 2867 abid2f 2921 abeq2f 2922 elabgt 3479 elabgf 3480 ralab2 3504 rexab2 3506 ss2ab 3803 ab0 4086 abn0 4089 sbccsb 4139 sbccsb2 4140 eluniab 4591 elintab 4631 iunab 4710 iinab 4725 zfrep4 4923 sniota 6031 opabiota 6415 eusvobj2 6798 eloprabga 6904 finds2 7251 wfrlem12 7587 en3lplem2 8673 scottexs 8915 scott0s 8916 cp 8919 cardprclem 8987 cfflb 9265 fin23lem29 9347 axdc3lem2 9457 4sqlem12 15854 xkococn 21657 ptcmplem4 22052 ofpreima 29766 qqhval2 30327 esum2dlem 30455 sigaclcu2 30484 bnj1143 31160 bnj1366 31199 bnj906 31299 bnj1256 31382 bnj1259 31383 bnj1311 31391 mclsax 31765 ellines 32557 bj-abeq2 33071 bj-csbsnlem 33196 topdifinffinlem 33498 finxpreclem6 33536 finxpnom 33541 setindtrs 38086 rababg 38373 compab 39139 tpid3gVD 39568 en3lplem2VD 39570 iunmapsn 39900 ssfiunibd 40014 setrec2lem2 42943 |
Copyright terms: Public domain | W3C validator |