Theorem inex2 5285

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454   ∩ cin 4092

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-in 4094

This theorem is used by:  ssexOLD  5290  wefrc  5652  hartogslem1  9573  setrec2fun  10010  infxpenlem  10131  dfac5lem5  10245  fin23lem12  10448  fpwwe2lem11  10765  cnso  16459  ressbas  17458  ressress  17469  rescabs  18058  symgvalstruct  19662  mgpress  20421  pjfval  22067  tgdom  23351  distop  23368  ustfilxp  24587  elovolmlem  25850  dyadmbl  25976  volsup2  25981  vitali  25989  itg1climres  26090  tayl0  26746  atomli  33041  ldgenpisyslem1  34907  reprinfz1  35362  dfac15  35886  vonf1onprcf1ac  36085  dfttc4  37533  bj-elid4  38357  aomclem6  44327  elinintrab  44839  isotone2  45310  ntrrn  45383  ntrf  45384  dssmapntrcls  45389  ismnushort  45546  onfrALTlem3  45787  sswfaxreg  46241  limcresiooub  46925  limcresioolb  46926  limsupval4  47077  sge0iunmptlemre  47698  ovolval2lem  47926  ovolval4lem2  47933  numtowerdt  48189