Theorem abbi2dv 2953

Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) Avoid ax-11 2160. (Revised by Wolf Lammen, 6-May-2023.)

Hypothesis

Ref	Expression
abbi2dv.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))

Assertion

Ref	Expression
abbi2dv	⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem abbi2dv

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		abbi2dv.1	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))
2	1	sbbidv 2083	. . 3 ⊢ (𝜑 → ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝜓))
3		clelsb3 2943	. . . 4 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
4	3	bicomi 226	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑥 ∈ 𝐴)
5		df-clab 2803	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
6	2, 4, 5	3bitr4g 316	. 2 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ {𝑥 ∣ 𝜓}))
7	6	eqrdv 2822	1 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1536  [wsb 2068   ∈ wcel 2113  {cab 2802

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896

This theorem is referenced by:  abbi1dv  2955  abbi2i  2956  sbab  2963  iftrue  4476  iffalse  4479  dfopif  4803  iniseg  5963  setlikespec  6172  fncnvima2  6834  isoini  7094  dftpos3  7913  mapsnd  8453  hartogslem1  9009  r1val2  9269  cardval2  9423  dfac3  9550  wrdval  13867  wrdnval  13899  submacs  17994  ablsimpgfind  19235  dfrhm2  19472  lsppr  19868  rspsn  20030  znunithash  20714  tgval3  21574  txrest  22242  xkoptsub  22265  cnextf  22677  cnblcld  23386  shft2rab  24112  sca2rab  24116  grpoinvf  28312  elpjrn  29970  ofrn2  30390  neibastop3  33714  ecres2  35540  lkrval2  36230  lshpset2N  36259  hdmapoc  39071  submgmacs  44078