Theorem abbi1dv 2878

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 222	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))
3	2	abbi2dv 2877	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})
4	3	eqcomd 2744	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2106  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816

This theorem is referenced by:  rabeqcda  3429  abidnf  3638  csbtt  3849  csbie2g  3875  csbvarg  4365  iinxsng  5017  predep  6233  fnsnfv  6847  enfin2i  10077  fin1a2lem11  10166  hashf1  14171  shftuz  14780  psrbaglefi  21135  psrbaglefiOLD  21136  vmappw  26265  addsid1  34127  hdmap1fval  39810  hdmapfval  39841  hgmapfval  39900