Theorem abbi1dv 2954

Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)

Hypothesis

Ref	Expression
abbi1dv.1	⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴))

Assertion

Ref	Expression
abbi1dv	⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴)

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem abbi1dv

Step	Hyp	Ref	Expression
1		abbi1dv.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴))
2	1	bicomd 225	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))
3	2	abbi2dv 2952	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})
4	3	eqcomd 2829	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴)

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114  {cab 2801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895

This theorem is referenced by:  abidnf  3696  csbtt  3902  csbie2g  3925  csbvarg  4385  iinxsng  5012  predep  6176  enfin2i  9745  fin1a2lem11  9834  hashf1  13818  shftuz  14430  psrbaglefi  20154  vmappw  25695  hdmap1fval  38934  hdmapfval  38965  hgmapfval  39024  rabeqcda  39113