Theorem eqabdv 2866

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  [wsb 2067   ∈ wcel 2113  {cab 2711

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808

This theorem is referenced by:  eqabcdv  2867  eqabi  2868  sbab  2879  rabeqcda  3407  iftrue  4482  iffalse  4485  dfopif  4823  iniseg  6053  setlikespec  6280  fncnvima2  7003  isoini  7281  dftpos3  8183  elecreseq  8680  mapsnd  8820  hartogslem1  9439  r1val2  9741  cardval2  9895  dfac3  10023  wrdval  14430  wrdnval  14459  submgmacs  18633  submacs  18743  ablsimpgfind  20032  dfrhm2  20401  lsppr  21036  rspsn  21279  znunithash  21510  tgval3  22898  txrest  23566  xkoptsub  23589  cnextf  24001  cnblcld  24709  shft2rab  25456  sca2rab  25460  renegscl  28420  grpoinvf  30533  elpjrn  32191  ofrn2  32644  ellcsrspsn  35757  neibastop3  36478  ec1cnvres  38381  ecun  38490  lkrval2  39262  lshpset2N  39291  hdmapoc  42103