![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqabcdv | 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 |
---|---|
eqabcdv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴)) |
Ref | Expression |
---|---|
eqabcdv | ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqabcdv.1 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴)) | |
2 | 1 | bicomd 223 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) |
3 | 2 | eqabdv 2873 | . 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) |
4 | 3 | eqcomd 2741 | 1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 = wceq 1537 ∈ wcel 2106 {cab 2712 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 |
This theorem is referenced by: abidnf 3711 csbtt 3925 csbie2g 3951 csbvarg 4440 iinxsng 5093 predep 6353 fnsnfv 6988 enfin2i 10359 fin1a2lem11 10448 hashf1 14493 shftuz 15105 psrbaglefi 21964 vmappw 27174 addsrid 28012 mulsrid 28154 hdmap1fval 41779 hdmapfval 41810 hgmapfval 41869 |
Copyright terms: Public domain | W3C validator |