![]() |
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 5301 | . . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
3 | dfcleq 2721 | . . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵))) | |
4 | elin 3963 | . . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
5 | 4 | bibi2i 337 | . . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
6 | 5 | albii 1814 | . . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
7 | 3, 6 | bitri 275 | . . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
8 | 7 | exbii 1843 | . . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
9 | 2, 8 | mpbir 230 | . 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵) |
10 | 9 | issetri 3488 | 1 ⊢ (𝐴 ∩ 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 395 ∀wal 1532 = wceq 1534 ∃wex 1774 ∈ wcel 2099 Vcvv 3471 ∩ cin 3946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-sep 5299 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3473 df-in 3954 |
This theorem is referenced by: inex2 5318 inex1g 5319 inuni 5345 onfr 6408 ssimaex 6983 exfo 7115 ofmres 7988 fipwuni 9449 fisn 9450 elfiun 9453 dffi3 9454 marypha1lem 9456 epfrs 9754 tcmin 9764 bnd2 9916 kmlem13 10185 brdom3 10551 brdom5 10552 brdom4 10553 fpwwe 10669 canthwelem 10673 pwfseqlem4 10685 ingru 10838 ltweuz 13958 elrest 17408 invfval 17741 isoval 17747 isofn 17757 zeroofn 17977 zerooval 17983 catcval 18088 isacs5lem 18536 isunit 20311 isrhm 20416 rhmfn 20437 rhmval 20438 rhmsubclem1 20617 2idlval 21144 pjfval 21639 psdmul 22089 fctop 22906 cctop 22908 ppttop 22909 epttop 22911 mretopd 22995 toponmre 22996 tgrest 23062 resttopon 23064 restco 23067 ordtbas2 23094 cnrest2 23189 cnpresti 23191 cnprest 23192 cnprest2 23193 cmpsublem 23302 cmpsub 23303 connsuba 23323 1stcrest 23356 subislly 23384 cldllycmp 23398 lly1stc 23399 txrest 23534 basqtop 23614 fbssfi 23740 trfbas2 23746 snfil 23767 fgcl 23781 trfil2 23790 cfinfil 23796 csdfil 23797 supfil 23798 zfbas 23799 fin1aufil 23835 fmfnfmlem3 23859 flimrest 23886 hauspwpwf1 23890 fclsrest 23927 tmdgsum2 23999 tsmsval2 24033 tsmssubm 24046 ustuqtop2 24146 restmetu 24478 isnmhm 24662 icopnfhmeo 24867 iccpnfhmeo 24869 xrhmeo 24870 pi1buni 24966 minveclem3b 25355 uniioombllem2 25511 uniioombllem6 25516 vitali 25541 ellimc2 25805 limcflf 25809 taylfvallem 26291 taylf 26294 tayl0 26295 taylpfval 26298 xrlimcnp 26899 lrrecse 27858 ewlkle 29418 upgrewlkle2 29419 wlk1walk 29452 maprnin 32513 ordtprsval 33519 ordtprsuni 33520 ordtrestNEW 33522 ordtrest2NEWlem 33523 ordtrest2NEW 33524 ordtconnlem1 33525 xrge0iifhmeo 33537 eulerpartgbij 33992 eulerpartlemmf 33995 eulerpart 34002 ballotlemfrc 34146 cvmsss2 34884 cvmcov2 34885 mvrsval 35115 mpstval 35145 mclsind 35180 mthmpps 35192 dfon2lem4 35382 brapply 35534 neibastop1 35843 filnetlem3 35864 bj-restn0 36569 bj-restuni 36576 ptrest 37092 heiborlem3 37286 heibor 37294 polvalN 39378 fnwe2lem2 42475 harval3 42968 superficl 42997 ssficl 42999 trficl 43099 onfrALTlem5 43981 onfrALTlem5VD 44324 fourierdlem48 45542 fourierdlem49 45543 sge0resplit 45794 hoiqssbllem3 46012 rngcvalALTV 47327 rhmsubcALTVlem1 47343 ringcvalALTV 47351 |
Copyright terms: Public domain | W3C validator |