Theorem eqabcdv 2899

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 2898	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})
4	3	eqcomd 2771	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴)

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840

This theorem is used by:  abidnf  3667  csbtt  3871  csbie2g  3894  csbvarg  4399  iinxsng  5056  predep  6335  fnsnfv  6964  enfin2i  10320  fin1a2lem11  10409  hashf1  14514  shftuz  15132  psrbaglefi  22128  vmappw  27333  addsrid  28210  mulsrid  28359  kard0  35626  hdmap1fval  42630  hdmapfval  42661  hgmapfval  42720