Theorem inex2 5289

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

Syntax hints:   ∈ wcel 2149  Vcvv 3463   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-in 3920

This theorem is referenced by:  ssex  5292  wefrc  5656  hartogslem1  9504  infxpenlem  9997  dfac5lem5  10111  fin23lem12  10315  fpwwe2lem11  10626  cnso  16303  ressbas  17296  ressress  17307  rescabs  17890  symgvalstruct  19467  mgpress  20226  pjfval  21825  tgdom  23104  distop  23121  ustfilxp  24339  elovolmlem  25602  dyadmbl  25728  volsup2  25733  vitali  25741  itg1climres  25842  tayl0  26491  atomli  32675  ldgenpisyslem1  34498  reprinfz1  34954  dfttc4  36930  bj-elid4  37700  aomclem6  43678  elinintrab  44195  isotone2  44667  ntrrn  44740  ntrf  44741  dssmapntrcls  44746  ismnushort  44903  onfrALTlem3  45145  sswfaxreg  45588  limcresiooub  46248  limcresioolb  46249  limsupval4  46400  sge0iunmptlemre  47021  ovolval2lem  47249  ovolval4lem2  47256  nthrucw  47494  setrec2fun  50355