Theorem abbi2i 2464

Description: Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
abbiri.1	⊢ (x ∈ A ↔ φ)

Assertion

Ref	Expression
abbi2i	⊢ A = {x ∣ φ}

Distinct variable group:   x,A

Allowed substitution hint:   φ(x)

Proof of Theorem abbi2i

Step	Hyp	Ref	Expression
1		abeq2 2458	. 2 ⊢ (A = {x ∣ φ} ↔ ∀x(x ∈ A ↔ φ))
2		abbiri.1	. 2 ⊢ (x ∈ A ↔ φ)
3	1, 2	mpgbir 1550	1 ⊢ A = {x ∣ φ}

Syntax hints:   ↔ wb 176   = wceq 1642   ∈ wcel 1710  {cab 2339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349

This theorem is referenced by:  abid2  2470  cbvralcsf  3198  cbvreucsf  3200  cbvrabcsf  3201  dfdif2  3222  rabbi2dva  3463  symdif2  3520  dfnul2  3552  dfpr2  3749  dftp2  3772  0iin  4024  dfaddc2  4381  dfnnc2  4395  nnc0suc  4412  nncaddccl  4419  nnsucelrlem1  4424  nndisjeq  4429  preaddccan2lem1  4454  ltfinex  4464  ltfintrilem1  4465  ssfin  4470  ncfinraiselem2  4480  ncfinlowerlem1  4482  evenfinex  4503  oddfinex  4504  evenoddnnnul  4514  evenodddisjlem1  4515  nnadjoinlem1  4519  nnpweqlem1  4522  sfintfinlem1  4531  tfinnnlem1  4533  spfinex  4537  vfinspss  4551  vfinspclt  4552  vfinncsp  4554  dfop2lem2  4574  dfop2  4575  dfproj12  4576  dfproj22  4577  phialllem1  4616  setconslem6  4736  dfima2  4745  dfdm2  4900  dfdm3  4901  dfrn2  4902  dmun  4912  fv3  5341  epprc  5827  funsex  5828  pw1fnf1o  5855  fvfullfunlem1  5861  clos1ex  5876  qsexg  5982  mapexi  6003  fnpm  6008  enpw1pw  6075  nenpw1pwlem1  6084  ovmuc  6130  df0c2  6137  1cnc  6139  ovcelem1  6171  ce0nn  6180  leconnnc  6218  nclennlem1  6248  nnltp1clem1  6261  addccan2nclem2  6264  nmembers1lem1  6268  nncdiv3lem2  6276  nnc3n3p1  6278  nchoicelem11  6299  nchoicelem16  6304  nchoicelem18  6306  fnfreclem1  6317  dmsnfn  6327