Theorem eqabdv 2894

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  [wsb 2089   ∈ wcel 2141  {cab 2739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is referenced by:  eqabcdv  2895  eqabi  2896  sbab  2907  rabeqcda  3424  iftrue  4483  iffalse  4486  dfopif  4825  iniseg  6082  setlikespec  6307  fncnvima2  7037  isoini  7317  dftpos3  8218  elecreseq  8722  mapsnd  8862  hartogslem1  9484  r1val2  9789  cardval2  9943  dfac3  10071  wrdval  14523  wrdnval  14552  submgmacs  18742  submacs  18852  ablsimpgfind  20143  dfrhm2  20510  lsppr  21148  rspsn  21391  znunithash  21604  tgval3  23011  txrest  23679  xkoptsub  23702  cnextf  24114  cnblcld  24822  shft2rab  25558  sca2rab  25562  renegscl  28579  grpoinvf  30692  elpjrn  32350  ofrn2  32803  ellcsrspsn  35952  neibastop3  36683  ec1cnvres  38736  ecun  38853  disjimdmqseq  39269  lkrval2  39675  lshpset2N  39704  hdmapoc  42516