![]() |
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 4816 | . . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
3 | dfcleq 2645 | . . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵))) | |
4 | elin 3829 | . . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
5 | 4 | bibi2i 326 | . . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
6 | 5 | albii 1787 | . . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
7 | 3, 6 | bitri 264 | . . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
8 | 7 | exbii 1814 | . . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
9 | 2, 8 | mpbir 221 | . 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵) |
10 | 9 | issetri 3241 | 1 ⊢ (𝐴 ∩ 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 ∀wal 1521 = wceq 1523 ∃wex 1744 ∈ wcel 2030 Vcvv 3231 ∩ cin 3606 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-in 3614 |
This theorem is referenced by: inex2 4833 inex1g 4834 inuni 4856 predasetex 5733 onfr 5801 ssimaex 6302 exfo 6417 ofmres 7206 fipwuni 8373 fisn 8374 elfiun 8377 dffi3 8378 marypha1lem 8380 epfrs 8645 tcmin 8655 bnd2 8794 kmlem13 9022 brdom3 9388 brdom5 9389 brdom4 9390 fpwwe 9506 canthwelem 9510 pwfseqlem4 9522 ingru 9675 ltweuz 12800 elrest 16135 invfval 16466 isoval 16472 isofn 16482 zerooval 16696 catcval 16793 isacs5lem 17216 isunit 18703 isrhm 18769 2idlval 19281 pjfval 20098 fctop 20856 cctop 20858 ppttop 20859 epttop 20861 mretopd 20944 toponmre 20945 tgrest 21011 resttopon 21013 restco 21016 ordtbas2 21043 cnrest2 21138 cnpresti 21140 cnprest 21141 cnprest2 21142 cmpsublem 21250 cmpsub 21251 connsuba 21271 1stcrest 21304 subislly 21332 cldllycmp 21346 lly1stc 21347 txrest 21482 basqtop 21562 fbssfi 21688 trfbas2 21694 snfil 21715 fgcl 21729 trfil2 21738 cfinfil 21744 csdfil 21745 supfil 21746 zfbas 21747 fin1aufil 21783 fmfnfmlem3 21807 flimrest 21834 hauspwpwf1 21838 fclsrest 21875 tmdgsum2 21947 tsmsval2 21980 tsmssubm 21993 ustuqtop2 22093 metustfbas 22409 restmetu 22422 isnmhm 22597 icopnfhmeo 22789 iccpnfhmeo 22791 xrhmeo 22792 pi1buni 22886 minveclem3b 23245 uniioombllem2 23397 uniioombllem6 23402 vitali 23427 ellimc2 23686 limcflf 23690 taylfvallem 24157 taylf 24160 tayl0 24161 taylpfval 24164 xrlimcnp 24740 ewlkle 26557 upgrewlkle2 26558 wlk1walk 26591 maprnin 29634 ordtprsval 30092 ordtprsuni 30093 ordtrestNEW 30095 ordtrest2NEWlem 30096 ordtrest2NEW 30097 ordtconnlem1 30098 xrge0iifhmeo 30110 eulerpartgbij 30562 eulerpartlemmf 30565 eulerpart 30572 ballotlemfrc 30716 cvmsss2 31382 cvmcov2 31383 mvrsval 31528 mpstval 31558 mclsind 31593 mthmpps 31605 dfon2lem4 31815 brapply 32170 neibastop1 32479 filnetlem3 32500 bj-restn0 33168 bj-restuni 33175 ptrest 33538 heiborlem3 33742 heibor 33750 polvalN 35509 fnwe2lem2 37938 superficl 38189 ssficl 38191 trficl 38278 onfrALTlem5 39074 onfrALTlem5VD 39435 fourierdlem48 40689 fourierdlem49 40690 sge0resplit 40941 hoiqssbllem3 41159 rhmfn 42243 rhmval 42244 rngcvalALTV 42286 ringcvalALTV 42332 rhmsubclem1 42411 rhmsubcALTVlem1 42429 |
Copyright terms: Public domain | W3C validator |