Theorem inex2 5288

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459   ∩ cin 3925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933

This theorem is referenced by:  ssex  5291  wefrc  5648  hartogslem1  9556  infxpenlem  10027  dfac5lem5  10141  fin23lem12  10345  fpwwe2lem11  10655  cnso  16265  ressbas  17257  ressress  17268  rescabs  17846  symgvalstruct  19378  mgpress  20110  pjfval  21666  tgdom  22916  distop  22933  ustfilxp  24151  elovolmlem  25427  dyadmbl  25553  volsup2  25558  vitali  25566  itg1climres  25667  tayl0  26321  atomli  32363  ldgenpisyslem1  34194  reprinfz1  34654  bj-elid4  37186  aomclem6  43083  elinintrab  43601  isotone2  44073  ntrrn  44146  ntrf  44147  dssmapntrcls  44152  ismnushort  44325  onfrALTlem3  44569  sswfaxreg  45012  limcresiooub  45671  limcresioolb  45672  limsupval4  45823  sge0iunmptlemre  46444  ovolval2lem  46672  ovolval4lem2  46679  setrec2fun  49556