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

Theorem abeq2i 2543
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 2500 . 2  |-  ( x  e.  A  <->  x  e.  { x  |  ph }
)
3 abid 2424 . 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 1652    e. wcel 1725   {cab 2422
This theorem is referenced by:  rabid  2884  vex  2959  csbco  3260  csbnestgf  3299  pwss  3813  elsn  3829  snsspw  3970  iunpw  4759  funcnv3  5512  zfrep6  5968  opabiota  6538  tfrlem4  6640  tfrlem5  6641  tfrlem8  6645  tfrlem9  6646  tfrlem9a  6647  ixpn0  7094  mapsnen  7184  sbthlem1  7217  dffi3  7436  1idpr  8906  ltexprlem1  8913  ltexprlem2  8914  ltexprlem3  8915  ltexprlem4  8916  ltexprlem6  8918  ltexprlem7  8919  reclem2pr  8925  reclem3pr  8926  reclem4pr  8927  supsrlem  8986  isbasis2g  17013  txbas  17599  xkoccn  17651  xkoptsub  17686  xkoco1cn  17689  xkoco2cn  17690  xkoinjcn  17719  mbfi1fseqlem4  19610  avril1  21757  rnmpt2ss  24086  setinds  25405  wfrlem2  25539  wfrlem3  25540  wfrlem4  25541  wfrlem9  25546  frrlem2  25583  frrlem3  25584  frrlem4  25585  frrlem5e  25590  frrlem11  25594  sdclem1  26447  bnj1436  29211  bnj916  29304  bnj983  29322  bnj1083  29347  bnj1245  29383  bnj1311  29393  bnj1371  29398  bnj1398  29403  psubspset  30541  psubclsetN  30733
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432
  Copyright terms: Public domain W3C validator