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

Theorem inex2 5273
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 4159 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inex2.1 . . 3 𝐴 ∈ V
32inex1 5272 . 2 (𝐴𝐵) ∈ V
41, 3eqeltri 2834 1 (𝐵𝐴) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  Vcvv 3443  cin 3907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-sep 5254
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-v 3445  df-in 3915
This theorem is referenced by:  ssex  5276  wefrc  5625  hartogslem1  9436  infxpenlem  9907  dfac5lem5  10021  fin23lem12  10225  fpwwe2lem11  10535  cnso  16088  ressbas  17077  ressbasOLD  17078  ressress  17088  rescabs  17677  rescabsOLD  17678  symgvalstruct  19136  symgvalstructOLD  19137  mgpress  19869  mgpressOLD  19870  pjfval  21064  tgdom  22279  distop  22296  ustfilxp  23515  elovolmlem  24789  dyadmbl  24915  volsup2  24920  vitali  24928  itg1climres  25030  tayl0  25672  atomli  31152  ldgenpisyslem1  32565  reprinfz1  33038  bj-elid4  35570  aomclem6  41288  elinintrab  41753  isotone2  42225  ntrrn  42298  ntrf  42299  dssmapntrcls  42304  ismnushort  42485  onfrALTlem3  42730  limcresiooub  43777  limcresioolb  43778  limsupval4  43929  sge0iunmptlemre  44550  ovolval2lem  44778  ovolval4lem2  44785  setrec2fun  47031
  Copyright terms: Public domain W3C validator