![]() |
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 3948 | . 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵) | |
2 | inex2.1 | . . 3 ⊢ 𝐴 ∈ V | |
3 | 2 | inex1 4951 | . 2 ⊢ (𝐴 ∩ 𝐵) ∈ V |
4 | 1, 3 | eqeltri 2835 | 1 ⊢ (𝐵 ∩ 𝐴) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2139 Vcvv 3340 ∩ cin 3714 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-sep 4933 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-v 3342 df-in 3722 |
This theorem is referenced by: ssex 4954 wefrc 5260 hartogslem1 8614 infxpenlem 9046 dfac5lem5 9160 fin23lem12 9365 fpwwe2lem12 9675 cnso 15195 ressbas 16152 ressress 16160 rescabs 16714 mgpress 18720 pjfval 20272 tgdom 21004 distop 21021 ustfilxp 22237 elovolm 23463 elovolmr 23464 ovolmge0 23465 ovolgelb 23468 ovolunlem1a 23484 ovolunlem1 23485 ovoliunlem1 23490 ovoliunlem2 23491 ovolshftlem2 23498 ovolicc2 23510 ioombl1 23550 dyadmbl 23588 volsup2 23593 vitali 23601 itg1climres 23700 tayl0 24335 atomli 29571 ldgenpisyslem1 30556 reprinfz1 31030 aomclem6 38149 elinintrab 38403 isotone2 38867 ntrrn 38940 ntrf 38941 dssmapntrcls 38946 onfrALTlem3 39279 limcresiooub 40395 limcresioolb 40396 limsupval4 40547 sge0iunmptlemre 41153 ovolval2lem 41381 ovolval4lem2 41388 setrec2fun 42967 |
Copyright terms: Public domain | W3C validator |