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
Assertion
Ref Expression
inex2

Proof of Theorem inex2
StepHypRef Expression
1 incom 3534 . 2
2 inex2.1 . . 3
32inex1 4345 . 2
41, 3eqeltri 2507 1
 Colors of variables: wff set class Syntax hints:   wcel 1726  cvv 2957   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