![]() |
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 2714 | . 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑) | |
2 | sbid 2247 | . 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑) | |
3 | 1, 2 | bitri 274 | 1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 [wsb 2067 ∈ wcel 2106 {cab 2713 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-12 2171 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-sb 2068 df-clab 2714 |
This theorem is referenced by: eqabOLD 2878 eqabd 2880 abid2f 2939 eqabf 2940 elabgtOLD 3625 elabgf 3626 elabgOLD 3629 ralab2 3655 rexab2 3657 ss2ab 4016 ab0ALT 4336 abn0OLD 4341 sbccsb 4393 sbccsb2 4394 eluniab 4880 elintabOLD 4920 iunab 5011 iinab 5028 zfrep4 5253 rnep 5882 sniota 6487 opabiota 6924 eusvobj2 7349 eloprabga 7464 eloprabgaOLD 7465 finds2 7837 frrlem10 8226 wfrlem12OLD 8266 en3lplem2 9549 scottexs 9823 scott0s 9824 cp 9827 cardprclem 9915 cfflb 10195 fin23lem29 10277 axdc3lem2 10387 4sqlem12 16828 xkococn 23011 ptcmplem4 23406 noinfbnd1lem1 27071 ofpreima 31581 qqhval2 32563 esum2dlem 32691 sigaclcu2 32719 bnj1143 33402 bnj1366 33441 bnj906 33542 bnj1256 33627 bnj1259 33628 bnj1311 33636 mclsax 34163 ellines 34737 bj-csbsnlem 35370 bj-reabeq 35498 bj-velpwALT 35524 topdifinffinlem 35818 rdgssun 35849 finxpreclem6 35867 finxpnom 35872 ralssiun 35878 setindtrs 41335 rababg 41836 scottabf 42510 compab 42712 tpid3gVD 43114 en3lplem2VD 43116 iunmapsn 43428 ssfiunibd 43533 absnsb 45251 setrec2lem2 47129 |
Copyright terms: Public domain | W3C validator |