Theorem abbi2dv 2729

Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)

Hypothesis

Ref	Expression
abbi2dv.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem abbi2dv

Step	Hyp	Ref	Expression
1		abbi2dv.1	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))
2	1	alrimiv 1842	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜓))
3		abeq2 2719	. 2 ⊢ (𝐴 = {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜓))
4	2, 3	sylibr 223	1 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473   = wceq 1475   ∈ wcel 1977  {cab 2596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606

This theorem is referenced by:  abbi1dv  2730  sbab  2737  iftrue  4042  iffalse  4045  dfopif  4337  iniseg  5415  setlikespec  5618  fncnvima2  6247  isoini  6488  dftpos3  7257  hartogslem1  8330  r1val2  8583  cardval2  8700  dfac3  8827  wrdval  13163  wrdnval  13190  submacs  17188  dfrhm2  18540  lsppr  18914  rspsn  19075  znunithash  19732  tgval3  20578  txrest  21244  xkoptsub  21267  cnextf  21680  cnblcld  22388  shft2rab  23083  sca2rab  23087  grpoinvf  26770  elpjrn  28433  ofrn2  28822  neibastop3  31527  lkrval2  33395  lshpset2N  33424  hdmapoc  36241  mapsnd  38383  submgmacs  41594