Theorem eqabcdv 2894

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
eqabcdv.1	⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴))

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem eqabcdv

Step	Hyp	Ref	Expression
1		eqabcdv.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴))
2	1	bicomd 226	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))
3	2	eqabdv 2893	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})
4	3	eqcomd 2766	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴)

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

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 2732

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

This theorem is used by:  abidnf  3660  csbtt  3864  csbie2g  3887  csbvarg  4392  iinxsng  5048  predep  6328  fnsnfv  6958  enfin2i  10324  fin1a2lem11  10413  hashf1  14523  shftuz  15143  psrbaglefi  22142  vmappw  27353  addsrid  28230  mulsrid  28379  kard0  35681  hdmap1fval  42670  hdmapfval  42701  hgmapfval  42760