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

Theorem abeq2i 2198
Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.)
Hypothesis
Ref Expression
abeqi.1  |-  A  =  { x  |  ph }
Assertion
Ref Expression
abeq2i  |-  ( x  e.  A  <->  ph )

Proof of Theorem abeq2i
StepHypRef Expression
1 abeqi.1 . . 3  |-  A  =  { x  |  ph }
21eleq2i 2154 . 2  |-  ( x  e.  A  <->  x  e.  { x  |  ph }
)
3 abid 2076 . 2  |-  ( x  e.  { x  | 
ph }  <->  ph )
42, 3bitri 182 1  |-  ( x  e.  A  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 103    = wceq 1289    e. wcel 1438   {cab 2074
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084
This theorem is referenced by:  rabid  2542  vex  2622  csbco  2942  csbnestgf  2980  ifmdc  3428  pwss  3445  snsspw  3608  iunpw  4302  ordon  4303  funcnv3  5076  tfrlem4  6078  tfrlem8  6083  tfrlem9  6084  tfrlemibxssdm  6092  tfr1onlembxssdm  6108  tfrcllembxssdm  6121  mapsnen  6526  sbthlem1  6664  1idprl  7147  1idpru  7148  recexprlem1ssl  7190  recexprlem1ssu  7191  recexprlemss1l  7192  recexprlemss1u  7193
  Copyright terms: Public domain W3C validator