![]() |
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 2155. (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 2083 | . . 3 ⊢ (𝜑 → ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝜓)) |
3 | clelsb1 2861 | . . . 4 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | |
4 | 3 | bicomi 223 | . . 3 ⊢ (𝑦 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑥 ∈ 𝐴) |
5 | df-clab 2711 | . . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓) | |
6 | 2, 4, 5 | 3bitr4g 314 | . 2 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ {𝑥 ∣ 𝜓})) |
7 | 6 | eqrdv 2731 | 1 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 [wsb 2068 ∈ wcel 2107 {cab 2710 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 |
This theorem is referenced by: eqabcdv 2869 eqabi 2870 sbab 2883 rabeqcda 3444 iftrue 4533 iffalse 4536 dfopif 4869 iniseg 6093 setlikespec 6323 fncnvima2 7058 isoini 7330 dftpos3 8224 mapsnd 8876 hartogslem1 9533 r1val2 9828 cardval2 9982 dfac3 10112 wrdval 14463 wrdnval 14491 submacs 18704 ablsimpgfind 19972 dfrhm2 20242 lsppr 20692 rspsn 20879 znunithash 21104 tgval3 22448 txrest 23117 xkoptsub 23140 cnextf 23552 cnblcld 24273 shft2rab 25007 sca2rab 25011 grpoinvf 29763 elpjrn 31421 ofrn2 31843 neibastop3 35185 ecres2 37085 lkrval2 37898 lshpset2N 37927 hdmapoc 40740 submgmacs 46509 |
Copyright terms: Public domain | W3C validator |