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

Theorem inex2 4172
Description: Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
inex2.1  |-  A  e. 
_V
Assertion
Ref Expression
inex2  |-  ( B  i^i  A )  e. 
_V

Proof of Theorem inex2
StepHypRef Expression
1 incom 3374 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inex2.1 . . 3  |-  A  e. 
_V
32inex1 4171 . 2  |-  ( A  i^i  B )  e. 
_V
41, 3eqeltri 2366 1  |-  ( B  i^i  A )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801    i^i cin 3164
This theorem is referenced by:  ssex  4174  wefrc  4403  hartogslem1  7273  infxpenlem  7657  dfac5lem5  7770  fin23lem12  7973  fpwwe2lem12  8279  cnso  12541  ressbas  13214  ressress  13221  rescabs  13726  mgpress  15352  pjfval  16622  tgdom  16732  distop  16749  elovolm  18850  elovolmr  18851  ovolmge0  18852  ovolgelb  18855  ovolunlem1a  18871  ovolunlem1  18872  ovoliunlem1  18877  ovoliunlem2  18878  ovolshftlem2  18885  ovolicc2  18897  ioombl1  18935  dyadmbl  18971  volsup2  18976  vitali  18984  itg1climres  19085  atomli  22978  intvlset  25801  issubcat  25948  vtarsu  25989  aomclem6  27259  onfrALTlem3  28608
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-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172
  Copyright terms: Public domain W3C validator