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

Theorem inex2 5279
Description: Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
inex2.1 𝐴 ∈ V
Assertion
Ref Expression
inex2 (𝐵𝐴) ∈ V

Proof of Theorem inex2
StepHypRef Expression
1 incom 4165 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inex2.1 . . 3 𝐴 ∈ V
32inex1 5278 . 2 (𝐴𝐵) ∈ V
41, 3eqeltri 2830 1 (𝐵𝐴) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3447  cin 3913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5260
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3449  df-in 3921
This theorem is referenced by:  ssex  5282  wefrc  5631  hartogslem1  9486  infxpenlem  9957  dfac5lem5  10071  fin23lem12  10275  fpwwe2lem11  10585  cnso  16137  ressbas  17126  ressbasOLD  17127  ressress  17137  rescabs  17726  rescabsOLD  17727  symgvalstruct  19186  symgvalstructOLD  19187  mgpress  19919  mgpressOLD  19920  pjfval  21135  tgdom  22351  distop  22368  ustfilxp  23587  elovolmlem  24861  dyadmbl  24987  volsup2  24992  vitali  25000  itg1climres  25102  tayl0  25744  atomli  31373  ldgenpisyslem1  32826  reprinfz1  33299  bj-elid4  35689  aomclem6  41433  elinintrab  41941  isotone2  42413  ntrrn  42486  ntrf  42487  dssmapntrcls  42492  ismnushort  42673  onfrALTlem3  42918  limcresiooub  43973  limcresioolb  43974  limsupval4  44125  sge0iunmptlemre  44746  ovolval2lem  44974  ovolval4lem2  44981  setrec2fun  47227
  Copyright terms: Public domain W3C validator