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 5207 | . . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
3 | dfcleq 2817 | . . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵))) | |
4 | elin 4171 | . . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
5 | 4 | bibi2i 340 | . . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
6 | 5 | albii 1820 | . . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
7 | 3, 6 | bitri 277 | . . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
8 | 7 | exbii 1848 | . . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
9 | 2, 8 | mpbir 233 | . 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵) |
10 | 9 | issetri 3512 | 1 ⊢ (𝐴 ∩ 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∀wal 1535 = wceq 1537 ∃wex 1780 ∈ wcel 2114 Vcvv 3496 ∩ cin 3937 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-v 3498 df-in 3945 |
This theorem is referenced by: inex2 5224 inex1g 5225 inuni 5248 predasetex 6165 onfr 6232 ssimaex 6750 exfo 6873 ofmres 7687 fipwuni 8892 fisn 8893 elfiun 8896 dffi3 8897 marypha1lem 8899 epfrs 9175 tcmin 9185 bnd2 9324 kmlem13 9590 brdom3 9952 brdom5 9953 brdom4 9954 fpwwe 10070 canthwelem 10074 pwfseqlem4 10086 ingru 10239 ltweuz 13332 elrest 16703 invfval 17031 isoval 17037 isofn 17047 zerooval 17261 catcval 17358 isacs5lem 17781 isunit 19409 isrhm 19475 2idlval 20008 pjfval 20852 fctop 21614 cctop 21616 ppttop 21617 epttop 21619 mretopd 21702 toponmre 21703 tgrest 21769 resttopon 21771 restco 21774 ordtbas2 21801 cnrest2 21896 cnpresti 21898 cnprest 21899 cnprest2 21900 cmpsublem 22009 cmpsub 22010 connsuba 22030 1stcrest 22063 subislly 22091 cldllycmp 22105 lly1stc 22106 txrest 22241 basqtop 22321 fbssfi 22447 trfbas2 22453 snfil 22474 fgcl 22488 trfil2 22497 cfinfil 22503 csdfil 22504 supfil 22505 zfbas 22506 fin1aufil 22542 fmfnfmlem3 22566 flimrest 22593 hauspwpwf1 22597 fclsrest 22634 tmdgsum2 22706 tsmsval2 22740 tsmssubm 22753 ustuqtop2 22853 restmetu 23182 isnmhm 23357 icopnfhmeo 23549 iccpnfhmeo 23551 xrhmeo 23552 pi1buni 23646 minveclem3b 24033 uniioombllem2 24186 uniioombllem6 24191 vitali 24216 ellimc2 24477 limcflf 24481 taylfvallem 24948 taylf 24951 tayl0 24952 taylpfval 24955 xrlimcnp 25548 ewlkle 27389 upgrewlkle2 27390 wlk1walk 27422 maprnin 30469 ordtprsval 31163 ordtprsuni 31164 ordtrestNEW 31166 ordtrest2NEWlem 31167 ordtrest2NEW 31168 ordtconnlem1 31169 xrge0iifhmeo 31181 eulerpartgbij 31632 eulerpartlemmf 31635 eulerpart 31642 ballotlemfrc 31786 cvmsss2 32523 cvmcov2 32524 mvrsval 32754 mpstval 32784 mclsind 32819 mthmpps 32831 dfon2lem4 33033 brapply 33401 neibastop1 33709 filnetlem3 33730 bj-restn0 34383 bj-restuni 34390 ptrest 34893 heiborlem3 35093 heibor 35101 polvalN 37043 fnwe2lem2 39658 harval3 39911 superficl 39933 ssficl 39935 trficl 40021 onfrALTlem5 40883 onfrALTlem5VD 41226 fourierdlem48 42446 fourierdlem49 42447 sge0resplit 42695 hoiqssbllem3 42913 rhmfn 44196 rhmval 44197 rngcvalALTV 44239 ringcvalALTV 44285 rhmsubclem1 44364 rhmsubcALTVlem1 44382 |
Copyright terms: Public domain | W3C validator |