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

Theorem inex2 5318
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 4209 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inex2.1 . . 3 𝐴 ∈ V
32inex1 5317 . 2 (𝐴𝐵) ∈ V
41, 3eqeltri 2837 1 (𝐵𝐴) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2108  Vcvv 3480  cin 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958
This theorem is referenced by:  ssex  5321  wefrc  5679  hartogslem1  9582  infxpenlem  10053  dfac5lem5  10167  fin23lem12  10371  fpwwe2lem11  10681  cnso  16283  ressbas  17280  ressbasOLD  17281  ressress  17293  rescabs  17877  rescabsOLD  17878  symgvalstruct  19414  symgvalstructOLD  19415  mgpress  20147  pjfval  21726  tgdom  22985  distop  23002  ustfilxp  24221  elovolmlem  25509  dyadmbl  25635  volsup2  25640  vitali  25648  itg1climres  25749  tayl0  26403  atomli  32401  ldgenpisyslem1  34164  reprinfz1  34637  bj-elid4  37169  aomclem6  43071  elinintrab  43590  isotone2  44062  ntrrn  44135  ntrf  44136  dssmapntrcls  44141  ismnushort  44320  onfrALTlem3  44564  sswfaxreg  45004  limcresiooub  45657  limcresioolb  45658  limsupval4  45809  sge0iunmptlemre  46430  ovolval2lem  46658  ovolval4lem2  46665  setrec2fun  49211
  Copyright terms: Public domain W3C validator