Theorem abeq2i 2277

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 2233	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ 𝜑})
3		abid 2153	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
4	2, 3	bitri 183	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Syntax hints:   ↔ wb 104   = wceq 1343   ∈ wcel 2136  {cab 2151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161

This theorem is referenced by:  rabid  2641  vex  2729  csbco  3055  csbcow  3056  csbnestgf  3097  ifmdc  3558  pwss  3575  snsspw  3744  iunpw  4458  ordon  4463  funcnv3  5250  tfrlem4  6281  tfrlem8  6286  tfrlem9  6287  tfrlemibxssdm  6295  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  ixpm  6696  mapsnen  6777  sbthlem1  6922  1idprl  7531  1idpru  7532  recexprlem1ssl  7574  recexprlem1ssu  7575  recexprlemss1l  7576  recexprlemss1u  7577  txbas  12898