Theorem eqabdv 2889

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1554  [wsb 2084   ∈ wcel 2136  {cab 2734

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831

This theorem is referenced by:  eqabcdv  2890  eqabi  2891  sbab  2902  rabeqcda  3419  iftrue  4480  iffalse  4483  dfopif  4822  iniseg  6076  setlikespec  6301  fncnvima2  7031  isoini  7311  dftpos3  8212  elecreseq  8716  mapsnd  8857  hartogslem1  9480  r1val2  9785  cardval2  9939  dfac3  10067  wrdval  14519  wrdnval  14548  submgmacs  18727  submacs  18837  ablsimpgfind  20128  dfrhm2  20495  lsppr  21133  rspsn  21376  znunithash  21589  tgval3  22996  txrest  23664  xkoptsub  23687  cnextf  24099  cnblcld  24807  shft2rab  25543  sca2rab  25547  renegscl  28561  grpoinvf  30674  elpjrn  32332  ofrn2  32785  ellcsrspsn  35939  neibastop3  36670  ec1cnvres  38723  ecun  38840  disjimdmqseq  39256  lkrval2  39662  lshpset2N  39691  hdmapoc  42503