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 4783 | . . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
3 | dfcleq 2616 | . . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵))) | |
4 | elin 3796 | . . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
5 | 4 | bibi2i 327 | . . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
6 | 5 | albii 1747 | . . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
7 | 3, 6 | bitri 264 | . . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
8 | 7 | exbii 1774 | . . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
9 | 2, 8 | mpbir 221 | . 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵) |
10 | 9 | issetri 3210 | 1 ⊢ (𝐴 ∩ 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 384 ∀wal 1481 = wceq 1483 ∃wex 1704 ∈ wcel 1990 Vcvv 3200 ∩ cin 3573 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 |
This theorem is referenced by: inex2 4800 inex1g 4801 inuni 4826 predasetex 5695 onfr 5763 ssimaex 6263 exfo 6377 ofmres 7164 fipwuni 8332 fisn 8333 elfiun 8336 dffi3 8337 marypha1lem 8339 epfrs 8607 tcmin 8617 bnd2 8756 kmlem13 8984 brdom3 9350 brdom5 9351 brdom4 9352 fpwwe 9468 canthwelem 9472 pwfseqlem4 9484 ingru 9637 ltweuz 12760 elrest 16088 invfval 16419 isoval 16425 isofn 16435 zerooval 16649 catcval 16746 isacs5lem 17169 isunit 18657 isrhm 18721 2idlval 19233 pjfval 20050 fctop 20808 cctop 20810 ppttop 20811 epttop 20813 mretopd 20896 toponmre 20897 tgrest 20963 resttopon 20965 restco 20968 ordtbas2 20995 cnrest2 21090 cnpresti 21092 cnprest 21093 cnprest2 21094 cmpsublem 21202 cmpsub 21203 connsuba 21223 1stcrest 21256 subislly 21284 cldllycmp 21298 lly1stc 21299 txrest 21434 basqtop 21514 fbssfi 21641 trfbas2 21647 snfil 21668 fgcl 21682 trfil2 21691 cfinfil 21697 csdfil 21698 supfil 21699 zfbas 21700 fin1aufil 21736 fmfnfmlem3 21760 flimrest 21787 hauspwpwf1 21791 fclsrest 21828 tmdgsum2 21900 tsmsval2 21933 tsmssubm 21946 ustuqtop2 22046 metustfbas 22362 restmetu 22375 isnmhm 22550 icopnfhmeo 22742 iccpnfhmeo 22744 xrhmeo 22745 pi1buni 22840 minveclem3b 23199 uniioombllem2 23351 uniioombllem6 23356 vitali 23382 ellimc2 23641 limcflf 23645 taylfvallem 24112 taylf 24115 tayl0 24116 taylpfval 24119 xrlimcnp 24695 ewlkle 26501 upgrewlkle2 26502 wlk1walk 26535 maprnin 29506 ordtprsval 29964 ordtprsuni 29965 ordtrestNEW 29967 ordtrest2NEWlem 29968 ordtrest2NEW 29969 ordtconnlem1 29970 xrge0iifhmeo 29982 eulerpartgbij 30434 eulerpartlemmf 30437 eulerpart 30444 ballotlemfrc 30588 cvmsss2 31256 cvmcov2 31257 mvrsval 31402 mpstval 31432 mclsind 31467 mthmpps 31479 dfon2lem4 31691 brapply 32045 neibastop1 32354 filnetlem3 32375 bj-restn0 33043 bj-restuni 33050 ptrest 33408 heiborlem3 33612 heibor 33620 polvalN 35191 fnwe2lem2 37621 superficl 37872 ssficl 37874 trficl 37961 onfrALTlem5 38757 onfrALTlem5VD 39121 fourierdlem48 40371 fourierdlem49 40372 sge0resplit 40623 hoiqssbllem3 40838 rhmfn 41918 rhmval 41919 rngcvalALTV 41961 ringcvalALTV 42007 rhmsubclem1 42086 rhmsubcALTVlem1 42104 |
Copyright terms: Public domain | W3C validator |