Theorem inex2 5319

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475   ∩ cin 3948

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 2704  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956

This theorem is referenced by:  ssex  5322  wefrc  5671  hartogslem1  9537  infxpenlem  10008  dfac5lem5  10122  fin23lem12  10326  fpwwe2lem11  10636  cnso  16190  ressbas  17179  ressbasOLD  17180  ressress  17193  rescabs  17782  rescabsOLD  17783  symgvalstruct  19264  symgvalstructOLD  19265  mgpress  20002  mgpressOLD  20003  pjfval  21261  tgdom  22481  distop  22498  ustfilxp  23717  elovolmlem  24991  dyadmbl  25117  volsup2  25122  vitali  25130  itg1climres  25232  tayl0  25874  atomli  31635  ldgenpisyslem1  33161  reprinfz1  33634  bj-elid4  36049  aomclem6  41801  elinintrab  42328  isotone2  42800  ntrrn  42873  ntrf  42874  dssmapntrcls  42879  ismnushort  43060  onfrALTlem3  43305  limcresiooub  44358  limcresioolb  44359  limsupval4  44510  sge0iunmptlemre  45131  ovolval2lem  45359  ovolval4lem2  45366  setrec2fun  47737