Theorem inex2 5254

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436   ∩ cin 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904

This theorem is referenced by:  ssex  5257  wefrc  5608  hartogslem1  9428  infxpenlem  9904  dfac5lem5  10018  fin23lem12  10222  fpwwe2lem11  10532  cnso  16156  ressbas  17147  ressress  17158  rescabs  17740  symgvalstruct  19309  mgpress  20068  pjfval  21643  tgdom  22893  distop  22910  ustfilxp  24128  elovolmlem  25402  dyadmbl  25528  volsup2  25533  vitali  25541  itg1climres  25642  tayl0  26296  atomli  32362  ldgenpisyslem1  34176  reprinfz1  34635  bj-elid4  37212  aomclem6  43162  elinintrab  43680  isotone2  44152  ntrrn  44225  ntrf  44226  dssmapntrcls  44231  ismnushort  44404  onfrALTlem3  44647  sswfaxreg  45090  limcresiooub  45750  limcresioolb  45751  limsupval4  45902  sge0iunmptlemre  46523  ovolval2lem  46751  ovolval4lem2  46758  nthrucw  46994  setrec2fun  49803