Theorem inex2 5278

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906

This theorem is used by:  ssexOLD  5283  wefrc  5645  hartogslem1  9536  setrec2fun  9973  infxpenlem  10092  dfac5lem5  10206  fin23lem12  10409  fpwwe2lem11  10726  cnso  16415  ressbas  17414  ressress  17425  rescabs  18008  symgvalstruct  19611  mgpress  20370  pjfval  22012  tgdom  23296  distop  23313  ustfilxp  24532  elovolmlem  25795  dyadmbl  25921  volsup2  25926  vitali  25934  itg1climres  26035  tayl0  26689  atomli  32984  ldgenpisyslem1  34796  reprinfz1  35251  vonf1onprcf1ac  35894  dfttc4  37318  bj-elid4  38089  aomclem6  44060  elinintrab  44577  isotone2  45048  ntrrn  45121  ntrf  45122  dssmapntrcls  45127  ismnushort  45284  onfrALTlem3  45526  sswfaxreg  45976  limcresiooub  46651  limcresioolb  46652  limsupval4  46803  sge0iunmptlemre  47424  ovolval2lem  47652  ovolval4lem2  47659  numtowerdt  47915