Theorem eqabcdv 2863

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 223	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))
3	2	eqabdv 2862	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})
4	3	eqcomd 2736	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804

This theorem is referenced by:  abidnf  3676  csbtt  3882  csbie2g  3905  csbvarg  4400  iinxsng  5055  predep  6306  fnsnfv  6943  enfin2i  10281  fin1a2lem11  10370  hashf1  14429  shftuz  15042  psrbaglefi  21842  vmappw  27033  addsrid  27878  mulsrid  28023  hdmap1fval  41797  hdmapfval  41828  hgmapfval  41887