Theorem eqabdv 2896

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2096   ∈ wcel 2143  {cab 2741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838

This theorem is referenced by:  eqabcdv  2897  eqabi  2898  sbab  2909  rabeqcda  3427  iftrue  4493  iffalse  4496  dfopif  4835  iniseg  6099  setlikespec  6326  fncnvima2  7056  isoini  7336  dftpos3  8236  elecreseq  8740  mapsnd  8880  hartogslem1  9500  r1val2  9805  cardval2  9973  dfac3  10101  wrdval  14549  wrdnval  14578  submgmacs  18770  submacs  18881  ablsimpgfind  20177  dfrhm2  20552  lsppr  21214  rspsn  21501  znunithash  21714  tgval3  23120  txrest  23788  xkoptsub  23811  cnextf  24223  cnblcld  24931  shft2rab  25667  sca2rab  25671  renegscl  28691  grpoinvf  30884  elpjrn  32542  ofrn2  32985  ellcsrspsn  36133  neibastop3  36873  ec1cnvres  38925  ecun  39042  disjimdmqseq  39458  lkrval2  39864  lshpset2N  39893  hdmapoc  42705