Theorem eqabdv 2894

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2099   ∈ wcel 2145  {cab 2739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is used by:  eqabcdv  2895  eqabi  2896  sbab  2907  rabeqcda  3424  iftrue  4488  iffalse  4491  dfopif  4830  iniseg  6095  setlikespec  6327  fncnvima2  7058  isoini  7344  dftpos3  8254  elecreseq  8760  mapsnd  8907  hartogslem1  9529  r1val2  9842  cardval2  10065  dfac3  10193  wrdval  14654  wrdnval  14683  submgmacs  18899  submacs  19016  ablsimpgfind  20319  dfrhm2  20697  lsppr  21361  rspsn  21650  znunithash  21863  tgval3  23274  txrest  23943  xkoptsub  23966  cnextf  24378  cnblcld  25086  shft2rab  25822  sca2rab  25826  renegscl  28877  grpoinvf  31127  elpjrn  32785  ofrn2  33227  ellcsrspsn  36385  neibastop3  37130  ec1cnvres  39188  ecun  39305  disjimdmqseq  39721  lkrval2  40127  lshpset2N  40156  hdmapoc  42968