Theorem eqabdv 2893

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  [wsb 2098   ∈ wcel 2144  {cab 2738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  eqabcdv  2894  eqabi  2895  sbab  2906  rabeqcda  3423  iftrue  4487  iffalse  4490  dfopif  4836  iniseg  6096  setlikespec  6330  fncnvima2  7063  isoini  7348  dftpos3  8266  elecreseq  8772  mapsnd  8919  hartogslem1  9541  r1val2  9854  cardval2  10077  dfac3  10205  wrdval  14666  wrdnval  14695  submgmacs  18913  submacs  19030  ablsimpgfind  20333  dfrhm2  20711  lsppr  21375  rspsn  21664  znunithash  21877  tgval3  23288  txrest  23957  xkoptsub  23980  cnextf  24392  cnblcld  25100  shft2rab  25836  sca2rab  25840  renegscl  28891  grpoinvf  31141  elpjrn  32799  ofrn2  33283  ellcsrspsn  36494  neibastop3  37244  ec1cnvres  39315  ecun  39432  disjimdmqseq  39848  lkrval2  40254  lshpset2N  40283  hdmapoc  43095