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

Theorem abeq2i 2515
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 2472 . 2  |-  ( x  e.  A  <->  x  e.  { x  |  ph }
)
3 abid 2396 . 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 2394
This theorem is referenced by:  rabid  2848  vex  2923  csbco  3224  csbnestgf  3263  pwss  3777  elsn  3793  snsspw  3934  iunpw  4722  funcnv3  5475  zfrep6  5931  opabiota  6501  tfrlem4  6603  tfrlem5  6604  tfrlem8  6608  tfrlem9  6609  tfrlem9a  6610  ixpn0  7057  mapsnen  7147  sbthlem1  7180  dffi3  7398  1idpr  8866  ltexprlem1  8873  ltexprlem2  8874  ltexprlem3  8875  ltexprlem4  8876  ltexprlem6  8878  ltexprlem7  8879  reclem2pr  8885  reclem3pr  8886  reclem4pr  8887  supsrlem  8946  isbasis2g  16972  txbas  17556  xkoccn  17608  xkoptsub  17643  xkoco1cn  17646  xkoco2cn  17647  xkoinjcn  17676  mbfi1fseqlem4  19567  avril1  21714  rnmpt2ss  24043  setinds  25352  wfrlem2  25475  wfrlem3  25476  wfrlem4  25477  wfrlem9  25482  wfrlem12  25485  frrlem2  25500  frrlem3  25501  frrlem4  25502  frrlem5e  25507  frrlem11  25511  sdclem1  26341  bnj1436  28921  bnj916  29014  bnj983  29032  bnj1083  29057  bnj1245  29093  bnj1311  29103  bnj1371  29108  bnj1398  29113  psubspset  30230  psubclsetN  30422
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 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404
  Copyright terms: Public domain W3C validator