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

Theorem inex2 4579
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 3677 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inex2.1 . . 3  |-  A  e. 
_V
32inex1 4578 . 2  |-  ( A  i^i  B )  e. 
_V
41, 3eqeltri 2538 1  |-  ( B  i^i  A )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823   _Vcvv 3106    i^i cin 3460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468
This theorem is referenced by:  ssex  4581  wefrc  4862  hartogslem1  7959  infxpenlem  8382  dfac5lem5  8499  fin23lem12  8702  fpwwe2lem12  9008  cnso  14064  ressbas  14773  ressress  14781  rescabs  15321  mgpress  17347  pjfval  18910  tgdom  19647  distop  19664  ustfilxp  20881  elovolm  22052  elovolmr  22053  ovolmge0  22054  ovolgelb  22057  ovolunlem1a  22073  ovolunlem1  22074  ovoliunlem1  22079  ovoliunlem2  22080  ovolshftlem2  22087  ovolicc2  22099  ioombl1  22138  dyadmbl  22175  volsup2  22180  vitali  22188  itg1climres  22287  tayl0  22923  atomli  27499  aomclem6  31244  limcresiooub  31887  limcresioolb  31888  onfrALTlem3  33710
  Copyright terms: Public domain W3C validator