MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abeq2i Unicode version

Theorem abeq2i 2511
Description: Equality of a class variable and a class abstraction (inference rule). (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 2468 . 2  |-  ( x  e.  A  <->  x  e.  { x  |  ph }
)
3 abid 2392 . 2  |-  ( x  e.  { x  | 
ph }  <->  ph )
42, 3bitri 241 1  |-  ( x  e.  A  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649    e. wcel 1721   {cab 2390
This theorem is referenced by:  rabid  2844  vex  2919  csbco  3220  csbnestgf  3259  pwss  3773  elsn  3789  snsspw  3930  iunpw  4718  funcnv3  5471  zfrep6  5927  opabiota  6497  tfrlem4  6599  tfrlem5  6600  tfrlem8  6604  tfrlem9  6605  tfrlem9a  6606  ixpn0  7053  mapsnen  7143  sbthlem1  7176  dffi3  7394  1idpr  8862  ltexprlem1  8869  ltexprlem2  8870  ltexprlem3  8871  ltexprlem4  8872  ltexprlem6  8874  ltexprlem7  8875  reclem2pr  8881  reclem3pr  8882  reclem4pr  8883  supsrlem  8942  isbasis2g  16968  txbas  17552  xkoccn  17604  xkoptsub  17639  xkoco1cn  17642  xkoco2cn  17643  xkoinjcn  17672  mbfi1fseqlem4  19563  avril1  21710  rnmpt2ss  24039  setinds  25348  wfrlem2  25471  wfrlem3  25472  wfrlem4  25473  wfrlem9  25478  wfrlem12  25481  frrlem2  25496  frrlem3  25497  frrlem4  25498  frrlem5e  25503  frrlem11  25507  sdclem1  26337  bnj1436  28917  bnj916  29010  bnj983  29028  bnj1083  29053  bnj1245  29089  bnj1311  29099  bnj1371  29104  bnj1398  29109  psubspset  30226  psubclsetN  30418
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator