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

Theorem abeq2i 2465
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 2422 . 2  |-  ( x  e.  A  <->  x  e.  { x  |  ph }
)
3 abid 2346 . 2  |-  ( x  e.  { x  | 
ph }  <->  ph )
42, 3bitri 240 1  |-  ( x  e.  A  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1642    e. wcel 1710   {cab 2344
This theorem is referenced by:  rabid  2792  vex  2867  csbco  3166  csbnestgf  3205  pwss  3715  elsn  3731  snsspw  3865  iunpw  4652  funcnv3  5393  zfrep6  5834  opabiota  6380  tfrlem4  6482  tfrlem5  6483  tfrlem8  6487  tfrlem9  6488  tfrlem9a  6489  ixpn0  6936  mapsnen  7026  sbthlem1  7059  dffi3  7274  1idpr  8743  ltexprlem1  8750  ltexprlem2  8751  ltexprlem3  8752  ltexprlem4  8753  ltexprlem6  8755  ltexprlem7  8756  reclem2pr  8762  reclem3pr  8763  reclem4pr  8764  supsrlem  8823  isbasis2g  16792  txbas  17368  xkoccn  17419  xkoptsub  17454  xkoco1cn  17457  xkoco2cn  17458  xkoinjcn  17487  mbfi1fseqlem4  19177  avril1  20948  rnmpt2ss  23290  setinds  24692  wfrlem2  24815  wfrlem3  24816  wfrlem4  24817  wfrlem9  24822  wfrlem12  24825  frrlem2  24840  frrlem3  24841  frrlem4  24842  frrlem5e  24847  frrlem11  24851  sdclem1  25777  bnj1436  28634  bnj916  28727  bnj983  28745  bnj1083  28770  bnj1245  28806  bnj1311  28816  bnj1371  28821  bnj1398  28826  psubspset  30002  psubclsetN  30194
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354
  Copyright terms: Public domain W3C validator