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 4711 | . . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
3 | dfcleq 2604 | . . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵))) | |
4 | elin 3758 | . . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
5 | 4 | bibi2i 326 | . . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
6 | 5 | albii 1737 | . . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
7 | 3, 6 | bitri 263 | . . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
8 | 7 | exbii 1764 | . . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
9 | 2, 8 | mpbir 220 | . 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵) |
10 | 9 | issetri 3183 | 1 ⊢ (𝐴 ∩ 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 ∀wal 1473 = wceq 1475 ∃wex 1695 ∈ wcel 1977 Vcvv 3173 ∩ cin 3539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-in 3547 |
This theorem is referenced by: inex2 4728 inex1g 4729 inuni 4753 predasetex 5612 onfr 5680 ssimaex 6173 exfo 6285 ofmres 7055 fipwuni 8215 fisn 8216 elfiun 8219 dffi3 8220 marypha1lem 8222 epfrs 8490 tcmin 8500 bnd2 8639 kmlem13 8867 brdom3 9231 brdom5 9232 brdom4 9233 fpwwe 9347 canthwelem 9351 pwfseqlem4 9363 ingru 9516 ltweuz 12622 elrest 15911 invfval 16242 isoval 16248 isofn 16258 zerooval 16472 catcval 16569 isacs5lem 16992 isunit 18480 isrhm 18544 2idlval 19054 pjfval 19869 fctop 20618 cctop 20620 ppttop 20621 epttop 20623 mretopd 20706 toponmre 20707 tgrest 20773 resttopon 20775 restco 20778 ordtbas2 20805 cnrest2 20900 cnpresti 20902 cnprest 20903 cnprest2 20904 cmpsublem 21012 cmpsub 21013 consuba 21033 1stcrest 21066 subislly 21094 cldllycmp 21108 lly1stc 21109 txrest 21244 basqtop 21324 fbssfi 21451 trfbas2 21457 snfil 21478 fgcl 21492 trfil2 21501 cfinfil 21507 csdfil 21508 supfil 21509 zfbas 21510 fin1aufil 21546 fmfnfmlem3 21570 flimrest 21597 hauspwpwf1 21601 fclsrest 21638 tmdgsum2 21710 tsmsval2 21743 tsmssubm 21756 ustuqtop2 21856 metustfbas 22172 restmetu 22185 isnmhm 22360 icopnfhmeo 22550 iccpnfhmeo 22552 xrhmeo 22553 pi1buni 22648 minveclem3b 23007 uniioombllem2 23157 uniioombllem6 23162 vitali 23188 ellimc2 23447 limcflf 23451 taylfvallem 23916 taylf 23919 tayl0 23920 taylpfval 23923 xrlimcnp 24495 maprnin 28894 ordtprsval 29292 ordtprsuni 29293 ordtrestNEW 29295 ordtrest2NEWlem 29296 ordtrest2NEW 29297 ordtconlem1 29298 xrge0iifhmeo 29310 eulerpartgbij 29761 eulerpartlemmf 29764 eulerpart 29771 ballotlemfrc 29915 cvmsss2 30510 cvmcov2 30511 mvrsval 30656 mpstval 30686 mclsind 30721 mthmpps 30733 dfon2lem4 30935 brapply 31215 neibastop1 31524 filnetlem3 31545 bj-restn0 32224 bj-restuni 32231 ptrest 32578 heiborlem3 32782 heibor 32790 polvalN 34209 fnwe2lem2 36639 superficl 36891 ssficl 36893 trficl 36980 onfrALTlem5 37778 onfrALTlem5VD 38143 fourierdlem48 39047 fourierdlem49 39048 sge0resplit 39299 hoiqssbllem3 39514 ewlkle 40807 upgrewlkle2 40808 1wlk1walk 40843 rhmfn 41708 rhmval 41709 rngcvalALTV 41753 ringcvalALTV 41799 rhmsubclem1 41878 rhmsubcALTVlem1 41897 |
Copyright terms: Public domain | W3C validator |