Theorem abeq2i 2199

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.)

Hypothesis

Ref	Expression
abeqi.1	⊢ 𝐴 = {𝑥 ∣ 𝜑}

Assertion

Ref	Expression
abeq2i	⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Proof of Theorem abeq2i

Step	Hyp	Ref	Expression
1		abeqi.1	. . 3 ⊢ 𝐴 = {𝑥 ∣ 𝜑}
2	1	eleq2i 2155	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ 𝜑})
3		abid 2077	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
4	2, 3	bitri 183	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Syntax hints:   ↔ wb 104   = wceq 1290   ∈ wcel 1439  {cab 2075

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 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085

This theorem is referenced by:  rabid  2543  vex  2623  csbco  2943  csbnestgf  2981  ifmdc  3432  pwss  3449  snsspw  3614  iunpw  4315  ordon  4316  funcnv3  5089  tfrlem4  6092  tfrlem8  6097  tfrlem9  6098  tfrlemibxssdm  6106  tfr1onlembxssdm  6122  tfrcllembxssdm  6135  ixpm  6501  mapsnen  6582  sbthlem1  6720  1idprl  7203  1idpru  7204  recexprlem1ssl  7246  recexprlem1ssu  7247  recexprlemss1l  7248  recexprlemss1u  7249