Theorem inex2 5281

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3453   ∩ cin 4091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5251

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3455  df-in 4093

This theorem is used by:  ssexOLD  5286  wefrc  5648  hartogslem1  9546  setrec2fun  9983  infxpenlem  10102  dfac5lem5  10216  fin23lem12  10419  fpwwe2lem11  10736  cnso  16427  ressbas  17426  ressress  17437  rescabs  18020  symgvalstruct  19623  mgpress  20382  pjfval  22024  tgdom  23308  distop  23325  ustfilxp  24544  elovolmlem  25807  dyadmbl  25933  volsup2  25938  vitali  25946  itg1climres  26047  tayl0  26701  atomli  32996  ldgenpisyslem1  34849  reprinfz1  35304  dfac15  35824  vonf1onprcf1ac  35998  dfttc4  37445  bj-elid4  38229  aomclem6  44201  elinintrab  44718  isotone2  45189  ntrrn  45262  ntrf  45263  dssmapntrcls  45268  ismnushort  45425  onfrALTlem3  45666  sswfaxreg  46116  limcresiooub  46791  limcresioolb  46792  limsupval4  46943  sge0iunmptlemre  47564  ovolval2lem  47792  ovolval4lem2  47799  numtowerdt  48055