Theorem abbi2dv 2742

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 1855	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜓))
3		abeq2 2732	. 2 ⊢ (𝐴 = {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜓))
4	2, 3	sylibr 224	1 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1481   = wceq 1483   ∈ wcel 1990  {cab 2608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618

This theorem is referenced by:  abbi1dv  2743  sbab  2750  iftrue  4092  iffalse  4095  dfopif  4399  iniseg  5496  setlikespec  5701  fncnvima2  6339  isoini  6588  dftpos3  7370  hartogslem1  8447  r1val2  8700  cardval2  8817  dfac3  8944  wrdval  13308  wrdnval  13335  submacs  17365  dfrhm2  18717  lsppr  19093  rspsn  19254  znunithash  19913  tgval3  20767  txrest  21434  xkoptsub  21457  cnextf  21870  cnblcld  22578  shft2rab  23276  sca2rab  23280  grpoinvf  27386  elpjrn  29049  ofrn2  29442  neibastop3  32357  ecres2  34044  lkrval2  34377  lshpset2N  34406  hdmapoc  37223  mapsnd  39388  submgmacs  41804