Theorem abbi2dv 2876

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.)

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		clelsb1 2866	. . . 4 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
4	3	bicomi 223	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑥 ∈ 𝐴)
5		df-clab 2716	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
6	2, 4, 5	3bitr4g 313	. 2 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ {𝑥 ∣ 𝜓}))
7	6	eqrdv 2736	1 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  [wsb 2068   ∈ wcel 2108  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817

This theorem is referenced by:  abbi1dv  2877  abbi2i  2878  sbab  2885  iftrue  4462  iffalse  4465  dfopifOLD  4798  iniseg  5994  setlikespec  6217  fncnvima2  6920  isoini  7189  dftpos3  8031  mapsnd  8632  hartogslem1  9231  r1val2  9526  cardval2  9680  dfac3  9808  wrdval  14148  wrdnval  14176  submacs  18380  ablsimpgfind  19628  dfrhm2  19876  lsppr  20270  rspsn  20438  znunithash  20684  tgval3  22021  txrest  22690  xkoptsub  22713  cnextf  23125  cnblcld  23844  shft2rab  24577  sca2rab  24581  grpoinvf  28795  elpjrn  30453  ofrn2  30878  addscllem1  34058  neibastop3  34478  ecres2  36341  lkrval2  37031  lshpset2N  37060  hdmapoc  39872  submgmacs  45246