![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > inex2 | Structured version Visualization version GIF version |
Description: Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.) |
Ref | Expression |
---|---|
inex2.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
inex2 | ⊢ (𝐵 ∩ 𝐴) ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | incom 4159 | . 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵) | |
2 | inex2.1 | . . 3 ⊢ 𝐴 ∈ V | |
3 | 2 | inex1 5272 | . 2 ⊢ (𝐴 ∩ 𝐵) ∈ V |
4 | 1, 3 | eqeltri 2834 | 1 ⊢ (𝐵 ∩ 𝐴) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3443 ∩ cin 3907 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 ax-sep 5254 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3406 df-v 3445 df-in 3915 |
This theorem is referenced by: ssex 5276 wefrc 5625 hartogslem1 9436 infxpenlem 9907 dfac5lem5 10021 fin23lem12 10225 fpwwe2lem11 10535 cnso 16088 ressbas 17077 ressbasOLD 17078 ressress 17088 rescabs 17677 rescabsOLD 17678 symgvalstruct 19136 symgvalstructOLD 19137 mgpress 19869 mgpressOLD 19870 pjfval 21064 tgdom 22279 distop 22296 ustfilxp 23515 elovolmlem 24789 dyadmbl 24915 volsup2 24920 vitali 24928 itg1climres 25030 tayl0 25672 atomli 31152 ldgenpisyslem1 32565 reprinfz1 33038 bj-elid4 35570 aomclem6 41288 elinintrab 41753 isotone2 42225 ntrrn 42298 ntrf 42299 dssmapntrcls 42304 ismnushort 42485 onfrALTlem3 42730 limcresiooub 43777 limcresioolb 43778 limsupval4 43929 sge0iunmptlemre 44550 ovolval2lem 44778 ovolval4lem2 44785 setrec2fun 47031 |
Copyright terms: Public domain | W3C validator |