Theorem eqabdv 2897

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2101   ∈ wcel 2147  {cab 2741

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839

This theorem is used by:  eqabcdv  2898  eqabi  2899  sbab  2910  rabeqcda  3427  iftrue  4491  iffalse  4494  dfopif  4842  iniseg  6113  setlikespec  6354  fncnvima2  7092  isoini  7377  dftpos3  8299  elecreseq  8805  mapsnd  8952  hartogslem1  9573  r1val2  9886  cardval2  10111  dfac3  10239  wrdval  14702  wrdnval  14731  submgmacs  18956  submacs  19073  ablsimpgfind  20377  dfrhm2  20755  lsppr  21419  rspsn  21708  znunithash  21925  tgval3  23336  txrest  24005  xkoptsub  24028  cnextf  24440  cnblcld  25148  shft2rab  25884  sca2rab  25888  renegscl  28941  grpoinvf  31191  elpjrn  32849  ofrn2  33332  ellcsrspsn  36614  neibastop3  37365  ec1cnvres  39474  ecun  39591  disjimdmqseq  40007  lkrval2  40413  lshpset2N  40442  hdmapoc  43254