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 2715 | . 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑) | |
2 | sbid 2253 | . 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑) | |
3 | 1, 2 | bitri 278 | 1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 [wsb 2070 ∈ wcel 2110 {cab 2714 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-sb 2071 df-clab 2715 |
This theorem is referenced by: abeq2 2869 abeq2d 2871 abbiOLD 2877 abid2f 2936 abeq2f 2937 elabgtOLD 3579 elabgf 3580 elabgOLD 3583 ralab2 3607 ralab2OLD 3608 rexab2 3610 rexab2OLD 3611 ss2ab 3970 ab0ALT 4288 abn0OLD 4293 sbccsb 4345 sbccsb2 4346 eluniab 4831 elintab 4867 iunab 4957 iinab 4973 zfrep4 5186 rnep 5793 sniota 6368 opabiota 6791 eusvobj2 7203 eloprabga 7315 eloprabgaOLD 7316 finds2 7675 frrlem10 8033 wfrlem12 8063 en3lplem2 9225 scottexs 9500 scott0s 9501 cp 9504 cardprclem 9592 cfflb 9870 fin23lem29 9952 axdc3lem2 10062 4sqlem12 16506 xkococn 22554 ptcmplem4 22949 ofpreima 30719 qqhval2 31641 esum2dlem 31769 sigaclcu2 31797 bnj1143 32480 bnj1366 32519 bnj906 32620 bnj1256 32705 bnj1259 32706 bnj1311 32714 mclsax 33241 noinfbnd1lem1 33660 ellines 34188 bj-csbsnlem 34822 bj-reabeq 34951 topdifinffinlem 35252 rdgssun 35283 finxpreclem6 35301 finxpnom 35306 ralssiun 35312 setindtrs 40548 rababg 40855 scottabf 41529 compab 41731 tpid3gVD 42133 en3lplem2VD 42135 iunmapsn 42428 ssfiunibd 42519 absnsb 44191 setrec2lem2 46069 |
Copyright terms: Public domain | W3C validator |