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

Theorem abeq2i 2390
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 2347 . 2  |-  ( x  e.  A  <->  x  e.  { x  |  ph }
)
3 abid 2271 . 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 1623    e. wcel 1684   {cab 2269
This theorem is referenced by:  rabid  2716  vex  2791  csbco  3090  csbnestgf  3129  pwss  3639  elsn  3655  snsspw  3784  iunpw  4570  funcnv3  5311  zfrep6  5748  opabiota  6293  tfrlem4  6395  tfrlem5  6396  tfrlem8  6400  tfrlem9  6401  tfrlem9a  6402  ixpn0  6848  mapsnen  6938  sbthlem1  6971  dffi3  7184  1idpr  8653  ltexprlem1  8660  ltexprlem2  8661  ltexprlem3  8662  ltexprlem4  8663  ltexprlem6  8665  ltexprlem7  8666  reclem2pr  8672  reclem3pr  8673  reclem4pr  8674  supsrlem  8733  isbasis2g  16686  txbas  17262  xkoccn  17313  xkoptsub  17348  xkoco1cn  17351  xkoco2cn  17352  xkoinjcn  17381  mbfi1fseqlem4  19073  avril1  20836  rnmpt2ss  23239  setinds  24134  wfrlem2  24257  wfrlem3  24258  wfrlem4  24259  wfrlem9  24264  wfrlem12  24267  frrlem2  24282  frrlem3  24283  frrlem4  24284  frrlem5e  24289  frrlem11  24293  sdclem1  26453  bnj1436  28872  bnj916  28965  bnj983  28983  bnj1083  29008  bnj1245  29044  bnj1311  29054  bnj1371  29059  bnj1398  29064  psubspset  29933  psubclsetN  30125
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator