![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > abbi1dv | Structured version Visualization version GIF version |
Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) |
Ref | Expression |
---|---|
abbi1dv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴)) |
Ref | Expression |
---|---|
abbi1dv | ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abbi1dv.1 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴)) | |
2 | 1 | bicomd 226 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) |
3 | 2 | abbi2dv 2927 | . 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) |
4 | 3 | eqcomd 2804 | 1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1538 ∈ wcel 2111 {cab 2776 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 |
This theorem is referenced by: abidnf 3642 csbtt 3845 csbie2g 3868 csb0 4314 csbvarg 4339 iinxsng 4973 predep 6142 enfin2i 9732 fin1a2lem11 9821 hashf1 13811 shftuz 14420 psrbaglefi 20610 vmappw 25701 hdmap1fval 39092 hdmapfval 39123 hgmapfval 39182 rabeqcda 39398 |
Copyright terms: Public domain | W3C validator |