Theorem abbi2i 2321

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

Syntax hints:   ↔ wb 105   = wceq 1373   ∈ wcel 2177  {cab 2192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202

This theorem is referenced by:  abid2  2327  cbvralcsf  3160  cbvrexcsf  3161  cbvreucsf  3162  cbvrabcsf  3163  symdifxor  3443  dfnul2  3466  dfpr2  3657  dftp2  3687  0iin  3992  pwpwab  4021  epse  4397  fv3  5612  fo1st  6256  fo2nd  6257  xp2  6272  tfrlem3  6410  tfr1onlem3  6437  mapsn  6790  ixpconstg  6807  ixp0x  6826  nnzrab  9416  nn0zrab  9417