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

Theorem inex2 5107
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 4094 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inex2.1 . . 3 𝐴 ∈ V
32inex1 5106 . 2 (𝐴𝐵) ∈ V
41, 3eqeltri 2877 1 (𝐵𝐴) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2079  Vcvv 3432  cin 3853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767  ax-sep 5088
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-v 3434  df-in 3861
This theorem is referenced by:  ssex  5109  wefrc  5429  hartogslem1  8842  infxpenlem  9274  dfac5lem5  9388  fin23lem12  9588  fpwwe2lem12  9898  cnso  15421  ressbas  16371  ressress  16379  rescabs  16920  mgpress  18928  pjfval  20520  tgdom  21258  distop  21275  ustfilxp  22492  elovolmlem  23746  dyadmbl  23872  volsup2  23877  vitali  23885  itg1climres  23986  tayl0  24621  atomli  29838  ldgenpisyslem1  30995  reprinfz1  31466  aomclem6  39095  elinintrab  39373  isotone2  39835  ntrrn  39908  ntrf  39909  dssmapntrcls  39914  onfrALTlem3  40369  limcresiooub  41419  limcresioolb  41420  limsupval4  41571  sge0iunmptlemre  42193  ovolval2lem  42421  ovolval4lem2  42428  setrec2fun  44229
  Copyright terms: Public domain W3C validator