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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450   ∩ 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 2732  ax-sep 5251

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906

This theorem is used by:  ssexOLD  5286  wefrc  5649  hartogslem1  9515  infxpenlem  10017  dfac5lem5  10131  fin23lem12  10334  fpwwe2lem11  10651  cnso  16336  ressbas  17329  ressress  17340  rescabs  17923  symgvalstruct  19525  mgpress  20284  pjfval  21920  tgdom  23204  distop  23221  ustfilxp  24440  elovolmlem  25703  dyadmbl  25829  volsup2  25834  vitali  25842  itg1climres  25943  tayl0  26599  atomli  32864  ldgenpisyslem1  34675  reprinfz1  35131  dfttc4  37150  bj-elid4  37921  aomclem6  43901  elinintrab  44418  isotone2  44890  ntrrn  44963  ntrf  44964  dssmapntrcls  44969  ismnushort  45126  onfrALTlem3  45368  sswfaxreg  45811  limcresiooub  46471  limcresioolb  46472  limsupval4  46623  sge0iunmptlemre  47244  ovolval2lem  47472  ovolval4lem2  47479  numtowerdt  47735  setrec2fun  50619