| 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 4209 | . 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵) | |
| 2 | inex2.1 | . . 3 ⊢ 𝐴 ∈ V | |
| 3 | 2 | inex1 5317 | . 2 ⊢ (𝐴 ∩ 𝐵) ∈ V |
| 4 | 1, 3 | eqeltri 2837 | 1 ⊢ (𝐵 ∩ 𝐴) ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 Vcvv 3480 ∩ cin 3950 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-in 3958 |
| This theorem is referenced by: ssex 5321 wefrc 5679 hartogslem1 9582 infxpenlem 10053 dfac5lem5 10167 fin23lem12 10371 fpwwe2lem11 10681 cnso 16283 ressbas 17280 ressbasOLD 17281 ressress 17293 rescabs 17877 rescabsOLD 17878 symgvalstruct 19414 symgvalstructOLD 19415 mgpress 20147 pjfval 21726 tgdom 22985 distop 23002 ustfilxp 24221 elovolmlem 25509 dyadmbl 25635 volsup2 25640 vitali 25648 itg1climres 25749 tayl0 26403 atomli 32401 ldgenpisyslem1 34164 reprinfz1 34637 bj-elid4 37169 aomclem6 43071 elinintrab 43590 isotone2 44062 ntrrn 44135 ntrf 44136 dssmapntrcls 44141 ismnushort 44320 onfrALTlem3 44564 sswfaxreg 45004 limcresiooub 45657 limcresioolb 45658 limsupval4 45809 sge0iunmptlemre 46430 ovolval2lem 46658 ovolval4lem2 46665 setrec2fun 49211 |
| Copyright terms: Public domain | W3C validator |