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

Theorem inex2 4760
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 3783 . 2 (𝐵𝐴) = (𝐴𝐵)
2 inex2.1 . . 3 𝐴 ∈ V
32inex1 4759 . 2 (𝐴𝐵) ∈ V
41, 3eqeltri 2694 1 (𝐵𝐴) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  Vcvv 3186  cin 3554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-in 3562
This theorem is referenced by:  ssex  4762  wefrc  5068  hartogslem1  8391  infxpenlem  8780  dfac5lem5  8894  fin23lem12  9097  fpwwe2lem12  9407  cnso  14901  ressbas  15851  ressress  15859  rescabs  16414  mgpress  18421  pjfval  19969  tgdom  20693  distop  20710  ustfilxp  21926  elovolm  23150  elovolmr  23151  ovolmge0  23152  ovolgelb  23155  ovolunlem1a  23171  ovolunlem1  23172  ovoliunlem1  23177  ovoliunlem2  23178  ovolshftlem2  23185  ovolicc2  23197  ioombl1  23237  dyadmbl  23274  volsup2  23279  vitali  23288  itg1climres  23387  tayl0  24020  atomli  29090  ldgenpisyslem1  30007  aomclem6  37109  elinintrab  37364  isotone2  37829  ntrrn  37902  ntrf  37903  dssmapntrcls  37908  onfrALTlem3  38241  limcresiooub  39278  limcresioolb  39279  sge0iunmptlemre  39939  ovolval2lem  40164  ovolval4lem2  40171  setrec2fun  41732
  Copyright terms: Public domain W3C validator