Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > abid | GIF version |
Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
abid | ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-clab 2124 | . 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑) | |
2 | sbid 1747 | . 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑) | |
3 | 1, 2 | bitri 183 | 1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∈ wcel 1480 [wsb 1735 {cab 2123 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-4 1487 ax-17 1506 ax-i9 1510 |
This theorem depends on definitions: df-bi 116 df-sb 1736 df-clab 2124 |
This theorem is referenced by: abeq2 2246 abeq2i 2248 abeq1i 2249 abeq2d 2250 abid2f 2304 elabgt 2820 elabgf 2821 ralab2 2843 rexab2 2845 sbccsbg 3026 sbccsb2g 3027 ss2ab 3160 abn0r 3382 abn0m 3383 tpid3g 3633 eluniab 3743 elintab 3777 iunab 3854 iinab 3869 intexabim 4072 iinexgm 4074 opm 4151 finds2 4510 dmmrnm 4753 sniota 5110 eusvobj2 5753 eloprabga 5851 indpi 7143 elabgf0 12973 |
Copyright terms: Public domain | W3C validator |