|   | 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 2875 | . 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) | 
| 4 | 3 | eqcomd 2743 | 1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 {cab 2714 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 | 
| This theorem is referenced by: abidnf 3708 csbtt 3916 csbie2g 3939 csbvarg 4434 iinxsng 5088 predep 6351 fnsnfv 6988 enfin2i 10361 fin1a2lem11 10450 hashf1 14496 shftuz 15108 psrbaglefi 21946 vmappw 27159 addsrid 27997 mulsrid 28139 hdmap1fval 41798 hdmapfval 41829 hgmapfval 41888 | 
| Copyright terms: Public domain | W3C validator |