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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457   ∩ cin 3905

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-in 3913

This theorem is used by:  ssexOLD  5294  wefrc  5657  hartogslem1  9511  infxpenlem  10013  dfac5lem5  10127  fin23lem12  10330  fpwwe2lem11  10643  cnso  16327  ressbas  17320  ressress  17331  rescabs  17914  symgvalstruct  19513  mgpress  20272  pjfval  21908  tgdom  23187  distop  23204  ustfilxp  24423  elovolmlem  25686  dyadmbl  25812  volsup2  25817  vitali  25825  itg1climres  25926  tayl0  26578  atomli  32807  ldgenpisyslem1  34620  reprinfz1  35076  dfttc4  37100  bj-elid4  37871  aomclem6  43846  elinintrab  44363  isotone2  44835  ntrrn  44908  ntrf  44909  dssmapntrcls  44914  ismnushort  45071  onfrALTlem3  45313  sswfaxreg  45756  limcresiooub  46416  limcresioolb  46417  limsupval4  46568  sge0iunmptlemre  47189  ovolval2lem  47417  ovolval4lem2  47424  nthrucw  47667  setrec2fun  50529