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

Theorem abeq2i 2548
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 2505 . 2  |-  ( x  e.  A  <->  x  e.  { x  |  ph }
)
3 abid 2429 . 2  |-  ( x  e.  { x  | 
ph }  <->  ph )
42, 3bitri 249 1  |-  ( x  e.  A  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1364    e. wcel 1761   {cab 2427
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437
This theorem is referenced by:  rabid  2895  vex  2973  csbco  3295  csbnestgf  3689  elsn  3888  funcnv3  5476  opabiota  5751  zfrep6  6544  tfrlem4  6834  tfrlem8  6839  tfrlem9  6840  ixpn0  7291  mapsnen  7383  sbthlem1  7417  dffi3  7677  1idpr  9194  ltexprlem1  9201  ltexprlem2  9202  ltexprlem3  9203  ltexprlem4  9204  ltexprlem6  9206  ltexprlem7  9207  reclem2pr  9213  reclem3pr  9214  reclem4pr  9215  supsrlem  9274  txbas  19099  xkoccn  19151  xkoptsub  19186  xkoco1cn  19189  xkoco2cn  19190  xkoinjcn  19219  mbfi1fseqlem4  21155  avril1  23591  rnmpt2ss  25927  setinds  27520  wfrlem2  27654  wfrlem3  27655  wfrlem4  27656  wfrlem9  27661  frrlem2  27698  frrlem3  27699  frrlem4  27700  frrlem5e  27705  frrlem11  27709  sdclem1  28564  csbcom2fi  28863  csbgfi  28864  bnj1436  31667  bnj916  31760  bnj983  31778  bnj1083  31803  bnj1245  31839  bnj1311  31849  bnj1371  31854  bnj1398  31859  bj-elsngl  32191  bj-projun  32217  bj-projval  32219
  Copyright terms: Public domain W3C validator