![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > inex1 | Structured version Visualization version Unicode 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 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
inex1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inex1.1 |
. . . 4
![]() ![]() ![]() ![]() | |
2 | 1 | zfauscl 4526 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | dfcleq 2444 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | elin 3616 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | bibi2i 315 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | albii 1690 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | bitri 253 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7 | exbii 1717 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 2, 8 | mpbir 213 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | issetri 3051 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-v 3046 df-in 3410 |
This theorem is referenced by: inex2 4544 inex1g 4545 inuni 4564 predasetex 5394 onfr 5461 ssimaex 5928 exfo 6038 ofmres 6786 fipwuni 7937 fisn 7938 elfiun 7941 dffi3 7942 marypha1lem 7944 epfrs 8212 tcmin 8222 bnd2 8361 kmlem13 8589 brdom3 8953 brdom5 8954 brdom4 8955 fpwwe 9068 canthwelem 9072 pwfseqlem4 9084 ingru 9237 ltweuz 12172 elrest 15319 invfval 15657 isoval 15663 isofn 15673 zerooval 15887 catcval 15984 isacs5lem 16408 isunit 17878 isrhm 17942 2idlval 18450 pjfval 19262 fctop 20012 cctop 20014 ppttop 20015 epttop 20017 mretopd 20101 toponmre 20102 tgrest 20168 resttopon 20170 restco 20173 ordtbas2 20200 cnrest2 20295 cnpresti 20297 cnprest 20298 cnprest2 20299 cmpsublem 20407 cmpsub 20408 consuba 20428 1stcrest 20461 subislly 20489 cldllycmp 20503 lly1stc 20504 txrest 20639 basqtop 20719 fbssfi 20845 trfbas2 20851 snfil 20872 fgcl 20886 trfil2 20895 cfinfil 20901 csdfil 20902 supfil 20903 zfbas 20904 fin1aufil 20940 fmfnfmlem3 20964 flimrest 20991 hauspwpwf1 20995 fclsrest 21032 tmdgsum2 21104 tsmsval2 21137 tsmssubm 21150 ustuqtop2 21250 metustfbas 21565 restmetu 21578 isnmhm 21760 icopnfhmeo 21964 iccpnfhmeo 21966 xrhmeo 21967 pi1buni 22064 minveclem3b 22363 minveclem3bOLD 22375 uniioombllem2 22533 uniioombllem2OLD 22534 uniioombllem6 22539 vitali 22564 ellimc2 22825 limcflf 22829 taylfvallem 23306 taylf 23309 tayl0 23310 taylpfval 23313 xrlimcnp 23887 maprnin 28309 ordtprsval 28717 ordtprsuni 28718 ordtrestNEW 28720 ordtrest2NEWlem 28721 ordtrest2NEW 28722 ordtconlem1 28723 xrge0iifhmeo 28735 eulerpartgbij 29198 eulerpartlemmf 29201 eulerpart 29208 ballotlemfrc 29352 ballotlemfrcOLD 29390 cvmsss2 29990 cvmcov2 29991 mvrsval 30136 mpstval 30166 mclsind 30201 mthmpps 30213 dfon2lem4 30425 brapply 30698 neibastop1 31008 filnetlem3 31029 ptrest 31932 heiborlem3 32138 heibor 32146 polvalN 33464 fnwe2lem2 35903 superficl 36165 ssficl 36167 trficl 36255 onfrALTlem5 36902 onfrALTlem5VD 37276 fourierdlem48 38012 fourierdlem49 38013 sge0resplit 38242 hoiqssbllem3 38440 ewlkle 39606 upgrewlkle2 39608 1wlk1walk 39630 rhmfn 39905 rhmval 39906 rngcvalALTV 39950 ringcvalALTV 39996 rhmsubclem1 40075 rhmsubcALTVlem1 40094 |
Copyright terms: Public domain | W3C validator |