Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  abeq2i GIF version

Theorem abeq2i 2226
 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
StepHypRef Expression
1 abeqi.1 . . 3 𝐴 = {𝑥𝜑}
21eleq2i 2182 . 2 (𝑥𝐴𝑥 ∈ {𝑥𝜑})
3 abid 2103 . 2 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
42, 3bitri 183 1 (𝑥𝐴𝜑)
 Colors of variables: wff set class Syntax hints:   ↔ wb 104   = wceq 1314   ∈ wcel 1463  {cab 2101 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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111 This theorem is referenced by:  rabid  2581  vex  2661  csbco  2982  csbnestgf  3020  ifmdc  3477  pwss  3494  snsspw  3659  iunpw  4369  ordon  4370  funcnv3  5153  tfrlem4  6176  tfrlem8  6181  tfrlem9  6182  tfrlemibxssdm  6190  tfr1onlembxssdm  6206  tfrcllembxssdm  6219  ixpm  6590  mapsnen  6671  sbthlem1  6811  1idprl  7362  1idpru  7363  recexprlem1ssl  7405  recexprlem1ssu  7406  recexprlemss1l  7407  recexprlemss1u  7408  txbas  12322
 Copyright terms: Public domain W3C validator