|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > eqabdv | Structured version Visualization version GIF version | ||
| Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) Avoid ax-11 2156. (Revised by Wolf Lammen, 6-May-2023.) | 
| Ref | Expression | 
|---|---|
| eqabdv.1 | ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) | 
| Ref | Expression | 
|---|---|
| eqabdv | ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | eqabdv.1 | . . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) | |
| 2 | 1 | sbbidv 2078 | . . 3 ⊢ (𝜑 → ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝜓)) | 
| 3 | clelsb1 2867 | . . . 4 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | |
| 4 | 3 | bicomi 224 | . . 3 ⊢ (𝑦 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑥 ∈ 𝐴) | 
| 5 | df-clab 2714 | . . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓) | |
| 6 | 2, 4, 5 | 3bitr4g 314 | . 2 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ {𝑥 ∣ 𝜓})) | 
| 7 | 6 | eqrdv 2734 | 1 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1539 [wsb 2063 ∈ wcel 2107 {cab 2713 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 | 
| This theorem is referenced by: eqabcdv 2875 eqabi 2876 sbab 2888 rabeqcda 3447 iftrue 4530 iffalse 4533 dfopif 4869 iniseg 6114 setlikespec 6345 fncnvima2 7080 isoini 7359 dftpos3 8270 mapsnd 8927 hartogslem1 9583 r1val2 9878 cardval2 10032 dfac3 10162 wrdval 14556 wrdnval 14584 submgmacs 18731 submacs 18841 ablsimpgfind 20131 dfrhm2 20475 lsppr 21093 rspsn 21344 znunithash 21584 tgval3 22971 txrest 23640 xkoptsub 23663 cnextf 24075 cnblcld 24796 shft2rab 25544 sca2rab 25548 renegscl 28431 grpoinvf 30552 elpjrn 32210 ofrn2 32651 ellcsrspsn 35647 neibastop3 36364 ecres2 38281 lkrval2 39092 lshpset2N 39121 hdmapoc 41934 | 
| Copyright terms: Public domain | W3C validator |