Theorem abbi2dv 2952

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  [wsb 2069   ∈ wcel 2114  {cab 2801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895

This theorem is referenced by:  abbi1dv  2954  abbi2i  2955  sbab  2962  iftrue  4475  iffalse  4478  dfopif  4802  iniseg  5962  setlikespec  6171  fncnvima2  6833  isoini  7093  dftpos3  7912  mapsnd  8452  hartogslem1  9008  r1val2  9268  cardval2  9422  dfac3  9549  wrdval  13867  wrdnval  13898  submacs  17993  ablsimpgfind  19234  dfrhm2  19471  lsppr  19867  rspsn  20029  znunithash  20713  tgval3  21573  txrest  22241  xkoptsub  22264  cnextf  22676  cnblcld  23385  shft2rab  24111  sca2rab  24115  grpoinvf  28311  elpjrn  29969  ofrn2  30389  neibastop3  33712  ecres2  35538  lkrval2  36228  lshpset2N  36257  hdmapoc  39069  submgmacs  44078