Theorem inex2 5268

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444   ∩ cin 3910

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918

This theorem is referenced by:  ssex  5271  wefrc  5625  hartogslem1  9471  infxpenlem  9942  dfac5lem5  10056  fin23lem12  10260  fpwwe2lem11  10570  cnso  16191  ressbas  17182  ressress  17193  rescabs  17775  symgvalstruct  19311  mgpress  20070  pjfval  21648  tgdom  22898  distop  22915  ustfilxp  24133  elovolmlem  25408  dyadmbl  25534  volsup2  25539  vitali  25547  itg1climres  25648  tayl0  26302  atomli  32361  ldgenpisyslem1  34146  reprinfz1  34606  bj-elid4  37149  aomclem6  43041  elinintrab  43559  isotone2  44031  ntrrn  44104  ntrf  44105  dssmapntrcls  44110  ismnushort  44283  onfrALTlem3  44527  sswfaxreg  44970  limcresiooub  45633  limcresioolb  45634  limsupval4  45785  sge0iunmptlemre  46406  ovolval2lem  46634  ovolval4lem2  46641  setrec2fun  49674