Theorem abbi2i 2767

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

Hypothesis

Ref	Expression
abbi2i.1	⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Assertion

Ref	Expression
abbi2i	⊢ 𝐴 = {𝑥 ∣ 𝜑}

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem abbi2i

Step	Hyp	Ref	Expression
1		abeq2 2761	. 2 ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑))
2		abbi2i.1	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)
3	1, 2	mpgbir 1766	1 ⊢ 𝐴 = {𝑥 ∣ 𝜑}

Syntax hints:   ↔ wb 196   = wceq 1523   ∈ wcel 2030  {cab 2637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647

This theorem is referenced by:  abid1  2773  cbvralcsf  3598  cbvreucsf  3600  cbvrabcsf  3601  dfsymdif2  3884  symdif2  3885  dfnul2  3950  dfpr2  4228  dftp2  4263  0iin  4610  pwpwab  4646  epse  5126  fv3  6244  fo1st  7230  fo2nd  7231  xp2  7247  tfrlem3  7519  mapsn  7941  ixpconstg  7959  ixp0x  7978  dfom4  8584  cardnum  8955  alephiso  8959  nnzrab  11443  nn0zrab  11444  qnnen  14986  h2hcau  27964  dfch2  28394  hhcno  28891  hhcnf  28892  pjhmopidm  29170  bdayfo  31953  madeval2  32061  fobigcup  32132  dfsingles2  32153  dfrecs2  32182  dfrdg4  32183  dfint3  32184  bj-snglinv  33085  ecres  34184  dfdm6  34212  compeq  38959