Theorem abeq2i 2148

Description: Equality of a class variable and a class abstraction (inference rule). (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 2104	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ 𝜑})
3		abid 2028	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
4	2, 3	bitri 173	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Syntax hints:   ↔ wb 98   = wceq 1243   ∈ wcel 1393  {cab 2026

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036

This theorem is referenced by:  rabid  2485  vex  2560  csbco  2861  csbnestgf  2898  pwss  3374  snsspw  3535  iunpw  4211  ordon  4212  funcnv3  4961  tfrlem4  5929  tfrlem8  5934  tfrlem9  5935  tfrlemibxssdm  5941  1idprl  6688  1idpru  6689  recexprlem1ssl  6731  recexprlem1ssu  6732  recexprlemss1l  6733  recexprlemss1u  6734