Theorem eqabdv 2865

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  [wsb 2065   ∈ wcel 2104  {cab 2707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808

This theorem is referenced by:  eqabcdv  2866  eqabi  2867  sbab  2880  rabeqcda  3441  iftrue  4533  iffalse  4536  dfopif  4869  iniseg  6095  setlikespec  6325  fncnvima2  7061  isoini  7337  dftpos3  8231  mapsnd  8882  hartogslem1  9539  r1val2  9834  cardval2  9988  dfac3  10118  wrdval  14471  wrdnval  14499  submgmacs  18642  submacs  18744  ablsimpgfind  20021  dfrhm2  20365  lsppr  20848  rspsn  21092  znunithash  21339  tgval3  22686  txrest  23355  xkoptsub  23378  cnextf  23790  cnblcld  24511  shft2rab  25257  sca2rab  25261  grpoinvf  30052  elpjrn  31710  ofrn2  32132  neibastop3  35550  ecres2  37450  lkrval2  38263  lshpset2N  38292  hdmapoc  41105