Theorem abbi2i 2738

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 2732	. 2 ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑))
2		abbi2i.1	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)
3	1, 2	mpgbir 1726	1 ⊢ 𝐴 = {𝑥 ∣ 𝜑}

Syntax hints:   ↔ wb 196   = 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:  abid1  2744  cbvralcsf  3565  cbvreucsf  3567  cbvrabcsf  3568  dfsymdif2  3851  symdif2  3852  dfnul2  3917  dfpr2  4195  dftp2  4231  0iin  4578  pwpwab  4614  epse  5097  fv3  6206  fo1st  7188  fo2nd  7189  xp2  7203  tfrlem3  7474  mapsn  7899  ixpconstg  7917  ixp0x  7936  dfom4  8546  cardnum  8917  alephiso  8921  nnzrab  11405  nn0zrab  11406  qnnen  14942  h2hcau  27836  dfch2  28266  hhcno  28763  hhcnf  28764  pjhmopidm  29042  bdayfo  31828  madeval2  31936  fobigcup  32007  dfsingles2  32028  dfrecs2  32057  dfrdg4  32058  dfint3  32059  bj-snglinv  32960  ecres  34043  dfdm6  34071  compeq  38642