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

Theorem inex2 5213
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 4175 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inex2.1 . . 3 𝐴 ∈ V
32inex1 5212 . 2 (𝐴𝐵) ∈ V
41, 3eqeltri 2906 1 (𝐵𝐴) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3492  cin 3932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-in 3940
This theorem is referenced by:  ssex  5216  wefrc  5542  hartogslem1  8994  infxpenlem  9427  dfac5lem5  9541  fin23lem12  9741  fpwwe2lem12  10051  cnso  15588  ressbas  16542  ressress  16550  rescabs  17091  mgpress  19179  pjfval  20778  tgdom  21514  distop  21531  ustfilxp  22748  elovolmlem  24002  dyadmbl  24128  volsup2  24133  vitali  24141  itg1climres  24242  tayl0  24877  atomli  30086  ldgenpisyslem1  31321  reprinfz1  31792  bj-elid4  34352  aomclem6  39537  elinintrab  39815  isotone2  40277  ntrrn  40350  ntrf  40351  dssmapntrcls  40356  onfrALTlem3  40755  limcresiooub  41799  limcresioolb  41800  limsupval4  41951  sge0iunmptlemre  42574  ovolval2lem  42802  ovolval4lem2  42809  setrec2fun  44723
  Copyright terms: Public domain W3C validator