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 225 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) |
3 | 2 | abbi2dv 2950 | . 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) |
4 | 3 | eqcomd 2827 | 1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1533 ∈ wcel 2110 {cab 2799 |
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 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1777 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 |
This theorem is referenced by: abidnf 3693 csbtt 3899 csbie2g 3922 csbvarg 4382 iinxsng 5002 predep 6168 enfin2i 9737 fin1a2lem11 9826 hashf1 13809 shftuz 14422 psrbaglefi 20146 vmappw 25687 hdmap1fval 38926 hdmapfval 38957 hgmapfval 39016 rabeqcda 39099 |
Copyright terms: Public domain | W3C validator |