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

Theorem inex2 4517
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 3593 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inex2.1 . . 3  |-  A  e. 
_V
32inex1 4516 . 2  |-  ( A  i^i  B )  e. 
_V
41, 3eqeltri 2526 1  |-  ( B  i^i  A )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1891   _Vcvv 3013    i^i cin 3371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-v 3015  df-in 3379
This theorem is referenced by:  ssex  4519  wefrc  4806  hartogslem1  8044  infxpenlem  8431  dfac5lem5  8545  fin23lem12  8748  fpwwe2lem12  9053  cnso  14310  ressbas  15190  ressress  15198  rescabs  15749  mgpress  17745  pjfval  19280  tgdom  20005  distop  20022  ustfilxp  21238  elovolm  22439  elovolmr  22440  ovolmge0  22441  ovolgelb  22444  ovolunlem1a  22460  ovolunlem1  22461  ovoliunlem1  22466  ovoliunlem2  22467  ovolshftlem2  22474  ovolicc2  22487  ioombl1  22527  dyadmbl  22570  volsup2  22575  vitali  22583  itg1climres  22684  tayl0  23329  atomli  28047  ldgenpisyslem1  28992  aomclem6  35919  elinintrab  36185  onfrALTlem3  36911  limcresiooub  37765  limcresioolb  37766  sge0iunmptlemre  38316  ovolval2lem  38528  ovolval4lem2  38535
  Copyright terms: Public domain W3C validator