Theorem inex2 5243

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 4136	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inex2.1	. . 3 ⊢ 𝐴 ∈ V
3	2	inex1 5242	. 2 ⊢ (𝐴 ∩ 𝐵) ∈ V
4	1, 3	eqeltri 2836	1 ⊢ (𝐵 ∩ 𝐴) ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3433   ∩ cin 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-in 3895

This theorem is referenced by:  ssex  5246  wefrc  5584  hartogslem1  9310  infxpenlem  9778  dfac5lem5  9892  fin23lem12  10096  fpwwe2lem11  10406  cnso  15965  ressbas  16956  ressbasOLD  16957  ressress  16967  rescabs  17556  rescabsOLD  17557  symgvalstruct  19013  symgvalstructOLD  19014  mgpress  19744  mgpressOLD  19745  pjfval  20922  tgdom  22137  distop  22154  ustfilxp  23373  elovolmlem  24647  dyadmbl  24773  volsup2  24778  vitali  24786  itg1climres  24888  tayl0  25530  atomli  30753  ldgenpisyslem1  32140  reprinfz1  32611  bj-elid4  35348  aomclem6  40891  elinintrab  41192  isotone2  41666  ntrrn  41739  ntrf  41740  dssmapntrcls  41745  ismnushort  41926  onfrALTlem3  42171  limcresiooub  43190  limcresioolb  43191  limsupval4  43342  sge0iunmptlemre  43960  ovolval2lem  44188  ovolval4lem2  44195  setrec2fun  46409