Theorem abeq2i 2349

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

This proof depends on syntax axioms:   ↔ wb 105   = wceq 1402   ∈ wcel 2209  {cab 2224

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234

This theorem is used by:  rabid  2727  vex  2824  csbco  3157  csbcow  3158  csbnestgf  3200  ifmdc  3683  pwss  3708  snsspw  3889  iunpw  4626  ordon  4633  funcnv3  5443  tfrlem4  6584  tfrlem8  6589  tfrlem9  6590  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  ixpm  7012  mapsnen  7100  sbthlem1  7274  1idprl  7957  1idpru  7958  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  txbas  15359