Theorem abbi2i 2209

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

Hypothesis

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

Assertion

Ref	Expression
abbi2i	⊢ 𝐴 = {𝑥 ∣ 𝜑}

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem abbi2i

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

Syntax hints:   ↔ wb 104   = wceq 1296   ∈ wcel 1445  {cab 2081

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091

This theorem is referenced by:  abid2  2215  cbvralcsf  3004  cbvrexcsf  3005  cbvreucsf  3006  cbvrabcsf  3007  symdifxor  3281  dfnul2  3304  dfpr2  3485  dftp2  3511  0iin  3810  pwpwab  3838  epse  4193  fv3  5363  fo1st  5966  fo2nd  5967  xp2  5981  tfrlem3  6114  tfr1onlem3  6141  mapsn  6487  ixpconstg  6504  ixp0x  6523  nnzrab  8872  nn0zrab  8873