Theorem inex2 5237

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

Step	Hyp	Ref	Expression
1		incom 4131	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inex2.1	. . 3 ⊢ 𝐴 ∈ V
3	2	inex1 5236	. 2 ⊢ (𝐴 ∩ 𝐵) ∈ V
4	1, 3	eqeltri 2835	1 ⊢ (𝐵 ∩ 𝐴) ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3422   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890

This theorem is referenced by:  ssex  5240  wefrc  5574  hartogslem1  9231  infxpenlem  9700  dfac5lem5  9814  fin23lem12  10018  fpwwe2lem11  10328  cnso  15884  ressbas  16873  ressbasOLD  16874  ressress  16884  rescabs  17464  symgvalstruct  18919  symgvalstructOLD  18920  mgpress  19650  mgpressOLD  19651  pjfval  20823  tgdom  22036  distop  22053  ustfilxp  23272  elovolmlem  24543  dyadmbl  24669  volsup2  24674  vitali  24682  itg1climres  24784  tayl0  25426  atomli  30645  ldgenpisyslem1  32031  reprinfz1  32502  bj-elid4  35266  aomclem6  40800  elinintrab  41074  isotone2  41548  ntrrn  41621  ntrf  41622  dssmapntrcls  41627  ismnushort  41808  onfrALTlem3  42053  limcresiooub  43073  limcresioolb  43074  limsupval4  43225  sge0iunmptlemre  43843  ovolval2lem  44071  ovolval4lem2  44078  setrec2fun  46284