Theorem eqabi 2465

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
eqabi	⊢ A = {x ∣ φ}

Distinct variable group:   x,A

Allowed substitution hint:   φ(x)

Proof of Theorem eqabi

Step	Hyp	Ref	Expression
1		eqabb 2459	. 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  2471  cbvralcsf  3199  cbvreucsf  3201  cbvrabcsf  3202  dfdif2  3223  rabbi2dva  3464  symdif2  3521  dfnul2  3553  dfpr2  3750  dftp2  3773  0iin  4025  dfaddc2  4382  dfnnc2  4396  nnc0suc  4413  nncaddccl  4420  nnsucelrlem1  4425  nndisjeq  4430  preaddccan2lem1  4455  ltfinex  4465  ltfintrilem1  4466  ssfin  4471  ncfinraiselem2  4481  ncfinlowerlem1  4483  evenfinex  4504  oddfinex  4505  evenoddnnnul  4515  evenodddisjlem1  4516  nnadjoinlem1  4520  nnpweqlem1  4523  sfintfinlem1  4532  tfinnnlem1  4534  spfinex  4538  vfinspss  4552  vfinspclt  4553  vfinncsp  4555  dfop2lem2  4575  dfop2  4576  dfproj12  4577  dfproj22  4578  phialllem1  4617  setconslem6  4737  dfima2  4746  dfdm2  4901  dfdm3  4902  dfrn2  4903  dmun  4913  fv3  5342  epprc  5828  funsex  5829  pw1fnf1o  5856  fvfullfunlem1  5862  clos1ex  5877  qsexg  5983  mapexi  6004  fnpm  6009  enpw1pw  6076  nenpw1pwlem1  6085  ovmuc  6131  df0c2  6138  1cnc  6140  ovcelem1  6172  ce0nn  6181  leconnnc  6219  nclennlem1  6249  nnltp1clem1  6262  addccan2nclem2  6265  nmembers1lem1  6269  nncdiv3lem2  6277  nnc3n3p1  6279  nchoicelem11  6300  nchoicelem16  6305  nchoicelem18  6307  fnfreclem1  6318  dmsnfn  6328