Theorem inex2 4760

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

Syntax hints:   ∈ wcel 1987  Vcvv 3186   ∩ cin 3554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-in 3562

This theorem is referenced by:  ssex  4762  wefrc  5068  hartogslem1  8391  infxpenlem  8780  dfac5lem5  8894  fin23lem12  9097  fpwwe2lem12  9407  cnso  14901  ressbas  15851  ressress  15859  rescabs  16414  mgpress  18421  pjfval  19969  tgdom  20693  distop  20710  ustfilxp  21926  elovolm  23150  elovolmr  23151  ovolmge0  23152  ovolgelb  23155  ovolunlem1a  23171  ovolunlem1  23172  ovoliunlem1  23177  ovoliunlem2  23178  ovolshftlem2  23185  ovolicc2  23197  ioombl1  23237  dyadmbl  23274  volsup2  23279  vitali  23288  itg1climres  23387  tayl0  24020  atomli  29090  ldgenpisyslem1  30007  aomclem6  37109  elinintrab  37364  isotone2  37829  ntrrn  37902  ntrf  37903  dssmapntrcls  37908  onfrALTlem3  38241  limcresiooub  39278  limcresioolb  39279  sge0iunmptlemre  39939  ovolval2lem  40164  ovolval4lem2  40171  setrec2fun  41732