![]() |
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 4202 | . 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵) | |
2 | inex2.1 | . . 3 ⊢ 𝐴 ∈ V | |
3 | 2 | inex1 5322 | . 2 ⊢ (𝐴 ∩ 𝐵) ∈ V |
4 | 1, 3 | eqeltri 2822 | 1 ⊢ (𝐵 ∩ 𝐴) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 Vcvv 3462 ∩ cin 3946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5304 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-in 3954 |
This theorem is referenced by: ssex 5326 wefrc 5676 hartogslem1 9585 infxpenlem 10056 dfac5lem5 10170 fin23lem12 10374 fpwwe2lem11 10684 cnso 16249 ressbas 17248 ressbasOLD 17249 ressress 17262 rescabs 17851 rescabsOLD 17852 symgvalstruct 19394 symgvalstructOLD 19395 mgpress 20132 mgpressOLD 20133 pjfval 21704 tgdom 22972 distop 22989 ustfilxp 24208 elovolmlem 25494 dyadmbl 25620 volsup2 25625 vitali 25633 itg1climres 25735 tayl0 26389 atomli 32315 ldgenpisyslem1 33996 reprinfz1 34468 bj-elid4 36875 aomclem6 42720 elinintrab 43244 isotone2 43716 ntrrn 43789 ntrf 43790 dssmapntrcls 43795 ismnushort 43975 onfrALTlem3 44220 limcresiooub 45263 limcresioolb 45264 limsupval4 45415 sge0iunmptlemre 46036 ovolval2lem 46264 ovolval4lem2 46271 setrec2fun 48438 |
Copyright terms: Public domain | W3C validator |