Theorem eqabdv 2869

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

Hypothesis

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

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem eqabdv

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqabdv.1	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))
2	1	sbbidv 2085	. . 3 ⊢ (𝜑 → ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝜓))
3		clelsb1 2863	. . . 4 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
4	3	bicomi 224	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑥 ∈ 𝐴)
5		df-clab 2715	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
6	2, 4, 5	3bitr4g 314	. 2 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ {𝑥 ∣ 𝜓}))
7	6	eqrdv 2734	1 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  [wsb 2068   ∈ wcel 2114  {cab 2714

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eqabcdv  2870  eqabi  2871  sbab  2882  rabeqcda  3400  iftrue  4472  iffalse  4475  dfopif  4813  iniseg  6062  setlikespec  6289  fncnvima2  7013  isoini  7293  dftpos3  8194  elecreseq  8693  mapsnd  8834  hartogslem1  9457  r1val2  9761  cardval2  9915  dfac3  10043  wrdval  14478  wrdnval  14507  submgmacs  18685  submacs  18795  ablsimpgfind  20087  dfrhm2  20454  lsppr  21088  rspsn  21331  znunithash  21544  tgval3  22928  txrest  23596  xkoptsub  23619  cnextf  24031  cnblcld  24739  shft2rab  25475  sca2rab  25479  renegscl  28490  grpoinvf  30603  elpjrn  32261  ofrn2  32713  ellcsrspsn  35823  neibastop3  36544  ec1cnvres  38597  ecun  38714  disjimdmqseq  39130  lkrval2  39536  lshpset2N  39565  hdmapoc  42377