Theorem eqabdv 2868

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  [wsb 2068   ∈ wcel 2107  {cab 2710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811

This theorem is referenced by:  eqabcdv  2869  eqabi  2870  sbab  2883  rabeqcda  3444  iftrue  4533  iffalse  4536  dfopif  4869  iniseg  6093  setlikespec  6323  fncnvima2  7058  isoini  7330  dftpos3  8224  mapsnd  8876  hartogslem1  9533  r1val2  9828  cardval2  9982  dfac3  10112  wrdval  14463  wrdnval  14491  submacs  18704  ablsimpgfind  19972  dfrhm2  20242  lsppr  20692  rspsn  20879  znunithash  21104  tgval3  22448  txrest  23117  xkoptsub  23140  cnextf  23552  cnblcld  24273  shft2rab  25007  sca2rab  25011  grpoinvf  29763  elpjrn  31421  ofrn2  31843  neibastop3  35185  ecres2  37085  lkrval2  37898  lshpset2N  37927  hdmapoc  40740  submgmacs  46509