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

Theorem abeq2i 2403
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 2360 . 2  |-  ( x  e.  A  <->  x  e.  { x  |  ph }
)
3 abid 2284 . 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 1632    e. wcel 1696   {cab 2282
This theorem is referenced by:  rabid  2729  vex  2804  csbco  3103  csbnestgf  3142  pwss  3652  elsn  3668  snsspw  3800  iunpw  4586  funcnv3  5327  zfrep6  5764  opabiota  6309  tfrlem4  6411  tfrlem5  6412  tfrlem8  6416  tfrlem9  6417  tfrlem9a  6418  ixpn0  6864  mapsnen  6954  sbthlem1  6987  dffi3  7200  1idpr  8669  ltexprlem1  8676  ltexprlem2  8677  ltexprlem3  8678  ltexprlem4  8679  ltexprlem6  8681  ltexprlem7  8682  reclem2pr  8688  reclem3pr  8689  reclem4pr  8690  supsrlem  8749  isbasis2g  16702  txbas  17278  xkoccn  17329  xkoptsub  17364  xkoco1cn  17367  xkoco2cn  17368  xkoinjcn  17397  mbfi1fseqlem4  19089  avril1  20852  rnmpt2ss  23254  setinds  24205  wfrlem2  24328  wfrlem3  24329  wfrlem4  24330  wfrlem9  24335  wfrlem12  24338  frrlem2  24353  frrlem3  24354  frrlem4  24355  frrlem5e  24360  frrlem11  24364  sdclem1  26556  bnj1436  29188  bnj916  29281  bnj983  29299  bnj1083  29324  bnj1245  29360  bnj1311  29370  bnj1371  29375  bnj1398  29380  psubspset  30555  psubclsetN  30747
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator