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

Theorem abeq2i 2553
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 2507 . 2  |-  ( x  e.  A  <->  x  e.  { x  |  ph }
)
3 abid 2431 . 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 1369    e. wcel 1756   {cab 2429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439
This theorem is referenced by:  rabid  2900  vex  2978  csbco  3301  csbnestgf  3695  elsn  3894  funcnv3  5482  opabiota  5757  zfrep6  6548  tfrlem4  6841  tfrlem8  6846  tfrlem9  6847  ixpn0  7298  mapsnen  7390  sbthlem1  7424  dffi3  7684  1idpr  9201  ltexprlem1  9208  ltexprlem2  9209  ltexprlem3  9210  ltexprlem4  9211  ltexprlem6  9213  ltexprlem7  9214  reclem2pr  9220  reclem3pr  9221  reclem4pr  9222  supsrlem  9281  txbas  19143  xkoccn  19195  xkoptsub  19230  xkoco1cn  19233  xkoco2cn  19234  xkoinjcn  19263  mbfi1fseqlem4  21199  avril1  23659  rnmpt2ss  25995  setinds  27594  wfrlem2  27728  wfrlem3  27729  wfrlem4  27730  wfrlem9  27735  frrlem2  27772  frrlem3  27773  frrlem4  27774  frrlem5e  27779  frrlem11  27783  sdclem1  28642  csbcom2fi  28941  csbgfi  28942  bnj1436  31836  bnj916  31929  bnj983  31947  bnj1083  31972  bnj1245  32008  bnj1311  32018  bnj1371  32023  bnj1398  32028  bj-ififc  32106  bj-elsngl  32464  bj-projun  32490  bj-projval  32492
  Copyright terms: Public domain W3C validator