Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > inex1 | Structured version Visualization version GIF version |
Description: Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
inex1.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
inex1 | ⊢ (𝐴 ∩ 𝐵) ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inex1.1 | . . . 4 ⊢ 𝐴 ∈ V | |
2 | 1 | zfauscl 5169 | . . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
3 | dfcleq 2792 | . . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵))) | |
4 | elin 3897 | . . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
5 | 4 | bibi2i 341 | . . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
6 | 5 | albii 1821 | . . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
7 | 3, 6 | bitri 278 | . . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
8 | 7 | exbii 1849 | . . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
9 | 2, 8 | mpbir 234 | . 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵) |
10 | 9 | issetri 3457 | 1 ⊢ (𝐴 ∩ 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 ∀wal 1536 = wceq 1538 ∃wex 1781 ∈ wcel 2111 Vcvv 3441 ∩ cin 3880 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 ax-sep 5167 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-in 3888 |
This theorem is referenced by: inex2 5186 inex1g 5187 inuni 5210 predasetex 6131 onfr 6198 ssimaex 6723 exfo 6848 ofmres 7667 fipwuni 8874 fisn 8875 elfiun 8878 dffi3 8879 marypha1lem 8881 epfrs 9157 tcmin 9167 bnd2 9306 kmlem13 9573 brdom3 9939 brdom5 9940 brdom4 9941 fpwwe 10057 canthwelem 10061 pwfseqlem4 10073 ingru 10226 ltweuz 13324 elrest 16693 invfval 17021 isoval 17027 isofn 17037 zerooval 17251 catcval 17348 isacs5lem 17771 isunit 19403 isrhm 19469 2idlval 19999 pjfval 20395 fctop 21609 cctop 21611 ppttop 21612 epttop 21614 mretopd 21697 toponmre 21698 tgrest 21764 resttopon 21766 restco 21769 ordtbas2 21796 cnrest2 21891 cnpresti 21893 cnprest 21894 cnprest2 21895 cmpsublem 22004 cmpsub 22005 connsuba 22025 1stcrest 22058 subislly 22086 cldllycmp 22100 lly1stc 22101 txrest 22236 basqtop 22316 fbssfi 22442 trfbas2 22448 snfil 22469 fgcl 22483 trfil2 22492 cfinfil 22498 csdfil 22499 supfil 22500 zfbas 22501 fin1aufil 22537 fmfnfmlem3 22561 flimrest 22588 hauspwpwf1 22592 fclsrest 22629 tmdgsum2 22701 tsmsval2 22735 tsmssubm 22748 ustuqtop2 22848 restmetu 23177 isnmhm 23352 icopnfhmeo 23548 iccpnfhmeo 23550 xrhmeo 23551 pi1buni 23645 minveclem3b 24032 uniioombllem2 24187 uniioombllem6 24192 vitali 24217 ellimc2 24480 limcflf 24484 taylfvallem 24953 taylf 24956 tayl0 24957 taylpfval 24960 xrlimcnp 25554 ewlkle 27395 upgrewlkle2 27396 wlk1walk 27428 maprnin 30493 ordtprsval 31271 ordtprsuni 31272 ordtrestNEW 31274 ordtrest2NEWlem 31275 ordtrest2NEW 31276 ordtconnlem1 31277 xrge0iifhmeo 31289 eulerpartgbij 31740 eulerpartlemmf 31743 eulerpart 31750 ballotlemfrc 31894 cvmsss2 32634 cvmcov2 32635 mvrsval 32865 mpstval 32895 mclsind 32930 mthmpps 32942 dfon2lem4 33144 brapply 33512 neibastop1 33820 filnetlem3 33841 bj-restn0 34505 bj-restuni 34512 ptrest 35056 heiborlem3 35251 heibor 35259 polvalN 37201 fnwe2lem2 39995 harval3 40244 superficl 40266 ssficl 40268 trficl 40370 onfrALTlem5 41248 onfrALTlem5VD 41591 fourierdlem48 42796 fourierdlem49 42797 sge0resplit 43045 hoiqssbllem3 43263 rhmfn 44542 rhmval 44543 rngcvalALTV 44585 ringcvalALTV 44631 rhmsubclem1 44710 rhmsubcALTVlem1 44728 |
Copyright terms: Public domain | W3C validator |