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

Theorem inex2 4952
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 3948 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inex2.1 . . 3 𝐴 ∈ V
32inex1 4951 . 2 (𝐴𝐵) ∈ V
41, 3eqeltri 2835 1 (𝐵𝐴) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2139  Vcvv 3340  cin 3714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722
This theorem is referenced by:  ssex  4954  wefrc  5260  hartogslem1  8614  infxpenlem  9046  dfac5lem5  9160  fin23lem12  9365  fpwwe2lem12  9675  cnso  15195  ressbas  16152  ressress  16160  rescabs  16714  mgpress  18720  pjfval  20272  tgdom  21004  distop  21021  ustfilxp  22237  elovolm  23463  elovolmr  23464  ovolmge0  23465  ovolgelb  23468  ovolunlem1a  23484  ovolunlem1  23485  ovoliunlem1  23490  ovoliunlem2  23491  ovolshftlem2  23498  ovolicc2  23510  ioombl1  23550  dyadmbl  23588  volsup2  23593  vitali  23601  itg1climres  23700  tayl0  24335  atomli  29571  ldgenpisyslem1  30556  reprinfz1  31030  aomclem6  38149  elinintrab  38403  isotone2  38867  ntrrn  38940  ntrf  38941  dssmapntrcls  38946  onfrALTlem3  39279  limcresiooub  40395  limcresioolb  40396  limsupval4  40547  sge0iunmptlemre  41153  ovolval2lem  41381  ovolval4lem2  41388  setrec2fun  42967
  Copyright terms: Public domain W3C validator