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

Theorem inex2 4446
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 3555 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inex2.1 . . 3  |-  A  e. 
_V
32inex1 4445 . 2  |-  ( A  i^i  B )  e. 
_V
41, 3eqeltri 2513 1  |-  ( B  i^i  A )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   _Vcvv 2984    i^i cin 3339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2986  df-in 3347
This theorem is referenced by:  ssex  4448  wefrc  4726  hartogslem1  7768  infxpenlem  8192  dfac5lem5  8309  fin23lem12  8512  fpwwe2lem12  8820  cnso  13541  ressbas  14240  ressress  14247  rescabs  14758  mgpress  16614  pjfval  18143  tgdom  18595  distop  18612  ustfilxp  19799  elovolm  20970  elovolmr  20971  ovolmge0  20972  ovolgelb  20975  ovolunlem1a  20991  ovolunlem1  20992  ovoliunlem1  20997  ovoliunlem2  20998  ovolshftlem2  21005  ovolicc2  21017  ioombl1  21055  dyadmbl  21092  volsup2  21097  vitali  21105  itg1climres  21204  tayl0  21839  atomli  25798  aomclem6  29424  onfrALTlem3  31264
  Copyright terms: Public domain W3C validator