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

Theorem inex2 4156
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 3361 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inex2.1 . . 3  |-  A  e. 
_V
32inex1 4155 . 2  |-  ( A  i^i  B )  e. 
_V
41, 3eqeltri 2353 1  |-  ( B  i^i  A )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788    i^i cin 3151
This theorem is referenced by:  ssex  4158  wefrc  4387  hartogslem1  7257  infxpenlem  7641  dfac5lem5  7754  fin23lem12  7957  fpwwe2lem12  8263  cnso  12525  ressbas  13198  ressress  13205  rescabs  13710  mgpress  15336  pjfval  16606  tgdom  16716  distop  16733  elovolm  18834  elovolmr  18835  ovolmge0  18836  ovolgelb  18839  ovolunlem1a  18855  ovolunlem1  18856  ovoliunlem1  18861  ovoliunlem2  18862  ovolshftlem2  18869  ovolicc2  18881  ioombl1  18919  dyadmbl  18955  volsup2  18960  vitali  18968  itg1climres  19069  atomli  22962  intvlset  25698  issubcat  25845  vtarsu  25886  aomclem6  27156  onfrALTlem3  28309
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-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator