![]() |
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 4094 | . 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵) | |
2 | inex2.1 | . . 3 ⊢ 𝐴 ∈ V | |
3 | 2 | inex1 5106 | . 2 ⊢ (𝐴 ∩ 𝐵) ∈ V |
4 | 1, 3 | eqeltri 2877 | 1 ⊢ (𝐵 ∩ 𝐴) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2079 Vcvv 3432 ∩ cin 3853 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-ext 2767 ax-sep 5088 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-v 3434 df-in 3861 |
This theorem is referenced by: ssex 5109 wefrc 5429 hartogslem1 8842 infxpenlem 9274 dfac5lem5 9388 fin23lem12 9588 fpwwe2lem12 9898 cnso 15421 ressbas 16371 ressress 16379 rescabs 16920 mgpress 18928 pjfval 20520 tgdom 21258 distop 21275 ustfilxp 22492 elovolmlem 23746 dyadmbl 23872 volsup2 23877 vitali 23885 itg1climres 23986 tayl0 24621 atomli 29838 ldgenpisyslem1 30995 reprinfz1 31466 aomclem6 39095 elinintrab 39373 isotone2 39835 ntrrn 39908 ntrf 39909 dssmapntrcls 39914 onfrALTlem3 40369 limcresiooub 41419 limcresioolb 41420 limsupval4 41571 sge0iunmptlemre 42193 ovolval2lem 42421 ovolval4lem2 42428 setrec2fun 44229 |
Copyright terms: Public domain | W3C validator |