Theorem abbi2dv 2919

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1522  [wsb 2042   ∈ wcel 2081  {cab 2775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863

This theorem is referenced by:  abbi1dv  2921  abbi2i  2922  sbab  2932  iftrue  4387  iffalse  4390  dfopif  4707  iniseg  5836  setlikespec  6044  fncnvima2  6696  isoini  6954  dftpos3  7761  mapsnd  8299  hartogslem1  8852  r1val2  9112  cardval2  9266  dfac3  9393  wrdval  13710  wrdnval  13742  submacs  17804  dfrhm2  19159  lsppr  19555  rspsn  19716  znunithash  20393  tgval3  21255  txrest  21923  xkoptsub  21946  cnextf  22358  cnblcld  23066  shft2rab  23792  sca2rab  23796  grpoinvf  28000  elpjrn  29658  ofrn2  30077  neibastop3  33320  ecres2  35087  lkrval2  35776  lshpset2N  35805  hdmapoc  38617  ablsimpgfind  40186  submgmacs  43573