Theorem abbi2dv 2889

Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) Avoid ax-11 2158. (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 2084	. . 3 ⊢ (𝜑 → ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝜓))
3		clelsb3 2879	. . . 4 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
4	3	bicomi 227	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑥 ∈ 𝐴)
5		df-clab 2736	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
6	2, 4, 5	3bitr4g 317	. 2 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ {𝑥 ∣ 𝜓}))
7	6	eqrdv 2756	1 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  [wsb 2069   ∈ wcel 2111  {cab 2735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830

This theorem is referenced by:  abbi1dv  2890  abbi2i  2891  sbab  2898  iftrue  4429  iffalse  4432  dfopifOLD  4761  iniseg  5937  setlikespec  6152  fncnvima2  6827  isoini  7091  dftpos3  7926  mapsnd  8481  hartogslem1  9052  r1val2  9312  cardval2  9466  dfac3  9594  wrdval  13929  wrdnval  13957  submacs  18070  ablsimpgfind  19313  dfrhm2  19553  lsppr  19946  rspsn  20108  znunithash  20345  tgval3  21676  txrest  22344  xkoptsub  22367  cnextf  22779  cnblcld  23489  shft2rab  24221  sca2rab  24225  grpoinvf  28427  elpjrn  30085  ofrn2  30512  addscllem1  33714  neibastop3  34134  ecres2  36010  lkrval2  36700  lshpset2N  36729  hdmapoc  39541  submgmacs  44840