Theorem eqabcdv 2871

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  abidnf  3662  csbtt  3868  csbie2g  3891  csbvarg  4388  iinxsng  5045  predep  6296  fnsnfv  6921  enfin2i  10243  fin1a2lem11  10332  hashf1  14392  shftuz  15004  psrbaglefi  21894  vmappw  27094  addsrid  27972  mulsrid  28121  hdmap1fval  42172  hdmapfval  42203  hgmapfval  42262