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  4628  ordon  4635  funcnv3  5446  tfrlem4  6588  tfrlem8  6593  tfrlem9  6594  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  ixpm  7016  mapsnen  7104  sbthlem1  7279  1idprl  7963  1idpru  7964  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1l  8008  recexprlemss1u  8009  txbas  15484