Theorem eqabdv 2861

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsb 2065   ∈ wcel 2109  {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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  eqabcdv  2862  eqabi  2863  sbab  2875  rabeqcda  3414  iftrue  4490  iffalse  4493  dfopif  4830  iniseg  6057  setlikespec  6286  fncnvima2  7015  isoini  7295  dftpos3  8200  elecreseq  8697  mapsnd  8836  hartogslem1  9471  r1val2  9766  cardval2  9920  dfac3  10050  wrdval  14457  wrdnval  14486  submgmacs  18620  submacs  18730  ablsimpgfind  20018  dfrhm2  20359  lsppr  20976  rspsn  21219  znunithash  21450  tgval3  22826  txrest  23494  xkoptsub  23517  cnextf  23929  cnblcld  24638  shft2rab  25385  sca2rab  25389  renegscl  28325  grpoinvf  30434  elpjrn  32092  ofrn2  32537  ellcsrspsn  35601  neibastop3  36323  lkrval2  39056  lshpset2N  39085  hdmapoc  41898