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

Theorem inex2 4346
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 3534 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inex2.1 . . 3  |-  A  e. 
_V
32inex1 4345 . 2  |-  ( A  i^i  B )  e. 
_V
41, 3eqeltri 2507 1  |-  ( B  i^i  A )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   _Vcvv 2957    i^i cin 3320
This theorem is referenced by:  ssex  4348  wefrc  4577  hartogslem1  7512  infxpenlem  7896  dfac5lem5  8009  fin23lem12  8212  fpwwe2lem12  8517  cnso  12847  ressbas  13520  ressress  13527  rescabs  14034  mgpress  15660  pjfval  16934  tgdom  17044  distop  17061  ustfilxp  18243  elovolm  19372  elovolmr  19373  ovolmge0  19374  ovolgelb  19377  ovolunlem1a  19393  ovolunlem1  19394  ovoliunlem1  19399  ovoliunlem2  19400  ovolshftlem2  19407  ovolicc2  19419  ioombl1  19457  dyadmbl  19493  volsup2  19498  vitali  19506  itg1climres  19607  atomli  23886  aomclem6  27135  onfrALTlem3  28631
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2959  df-in 3328
  Copyright terms: Public domain W3C validator