Theorem inex2 5188

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

Syntax hints:   ∈ wcel 2111  Vcvv 3409   ∩ cin 3857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-sep 5169

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-rab 3079  df-v 3411  df-in 3865

This theorem is referenced by:  ssex  5191  wefrc  5518  hartogslem1  9039  infxpenlem  9473  dfac5lem5  9587  fin23lem12  9791  fpwwe2lem11  10101  cnso  15648  ressbas  16612  ressress  16620  rescabs  17162  symgvalstruct  18592  mgpress  19318  pjfval  20471  tgdom  21678  distop  21695  ustfilxp  22913  elovolmlem  24174  dyadmbl  24300  volsup2  24305  vitali  24313  itg1climres  24414  tayl0  25056  atomli  30264  ldgenpisyslem1  31650  reprinfz1  32121  bj-elid4  34863  aomclem6  40376  elinintrab  40650  isotone2  41125  ntrrn  41198  ntrf  41199  dssmapntrcls  41204  onfrALTlem3  41623  limcresiooub  42650  limcresioolb  42651  limsupval4  42802  sge0iunmptlemre  43420  ovolval2lem  43648  ovolval4lem2  43655  setrec2fun  45613