| 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 5298 | . . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 3 | dfcleq 2730 | . . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵))) | |
| 4 | elin 3967 | . . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
| 5 | 4 | bibi2i 337 | . . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
| 6 | 5 | albii 1819 | . . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
| 7 | 3, 6 | bitri 275 | . . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
| 8 | 7 | exbii 1848 | . . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
| 9 | 2, 8 | mpbir 231 | . 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵) |
| 10 | 9 | issetri 3499 | 1 ⊢ (𝐴 ∩ 𝐵) ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∀wal 1538 = wceq 1540 ∃wex 1779 ∈ wcel 2108 Vcvv 3480 ∩ cin 3950 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-in 3958 |
| This theorem is referenced by: inex2 5318 inex1g 5319 inuni 5350 onfr 6423 ssimaex 6994 exfo 7125 ofmres 8009 fipwuni 9466 fisn 9467 elfiun 9470 dffi3 9471 marypha1lem 9473 epfrs 9771 tcmin 9781 bnd2 9933 kmlem13 10203 brdom3 10568 brdom5 10569 brdom4 10570 fpwwe 10686 canthwelem 10690 pwfseqlem4 10702 ingru 10855 ltweuz 14002 elrest 17472 invfval 17803 isoval 17809 isofn 17819 zeroofn 18034 zerooval 18040 catcval 18145 isacs5lem 18590 isunit 20373 isrhm 20478 rhmfn 20499 rhmval 20500 rhmsubclem1 20685 2idlval 21261 pjfval 21726 psdmul 22170 fctop 23011 cctop 23013 ppttop 23014 epttop 23016 mretopd 23100 toponmre 23101 tgrest 23167 resttopon 23169 restco 23172 ordtbas2 23199 cnrest2 23294 cnpresti 23296 cnprest 23297 cnprest2 23298 cmpsublem 23407 cmpsub 23408 connsuba 23428 1stcrest 23461 subislly 23489 cldllycmp 23503 lly1stc 23504 txrest 23639 basqtop 23719 fbssfi 23845 trfbas2 23851 snfil 23872 fgcl 23886 trfil2 23895 cfinfil 23901 csdfil 23902 supfil 23903 zfbas 23904 fin1aufil 23940 fmfnfmlem3 23964 flimrest 23991 hauspwpwf1 23995 fclsrest 24032 tmdgsum2 24104 tsmsval2 24138 tsmssubm 24151 ustuqtop2 24251 restmetu 24583 isnmhm 24767 icopnfhmeo 24974 iccpnfhmeo 24976 xrhmeo 24977 pi1buni 25073 minveclem3b 25462 uniioombllem2 25618 uniioombllem6 25623 vitali 25648 ellimc2 25912 limcflf 25916 taylfvallem 26399 taylf 26402 tayl0 26403 taylpfval 26406 xrlimcnp 27011 lrrecse 27975 ewlkle 29623 upgrewlkle2 29624 wlk1walk 29657 maprnin 32742 ordtprsval 33917 ordtprsuni 33918 ordtrestNEW 33920 ordtrest2NEWlem 33921 ordtrest2NEW 33922 ordtconnlem1 33923 xrge0iifhmeo 33935 eulerpartgbij 34374 eulerpartlemmf 34377 eulerpart 34384 ballotlemfrc 34529 cvmsss2 35279 cvmcov2 35280 mvrsval 35510 mpstval 35540 mclsind 35575 mthmpps 35587 dfon2lem4 35787 brapply 35939 neibastop1 36360 filnetlem3 36381 weiunfr 36468 bj-restn0 37091 bj-restuni 37098 ptrest 37626 heiborlem3 37820 heibor 37828 polvalN 39907 fnwe2lem2 43063 harval3 43551 superficl 43580 ssficl 43582 trficl 43682 onfrALTlem5 44562 onfrALTlem5VD 44905 fourierdlem48 46169 fourierdlem49 46170 sge0resplit 46421 hoiqssbllem3 46639 rngcvalALTV 48181 rhmsubcALTVlem1 48197 ringcvalALTV 48205 |
| Copyright terms: Public domain | W3C validator |