![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eluni2 | Structured version Visualization version GIF version |
Description: Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.) |
Ref | Expression |
---|---|
eluni2 | ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exancom 1857 | . 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥)) | |
2 | eluni 4916 | . 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) | |
3 | df-rex 3061 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥)) | |
4 | 1, 2, 3 | 3bitr4i 302 | 1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 ∃wex 1774 ∈ wcel 2099 ∃wrex 3060 ∪ cuni 4913 |
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 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rex 3061 df-v 3464 df-uni 4914 |
This theorem is referenced by: uni0b 4941 intssuni 4978 iuncom4 5009 inuni 5350 cnvuni 5893 chfnrn 7062 ssorduni 7787 unon 7840 limuni3 7862 frrlem9 8309 onfununi 8371 oarec 8592 uniinqs 8826 fissuni 9401 finsschain 9403 r1sdom 9817 rankuni2b 9896 cflm 10293 coflim 10304 axdc3lem2 10494 fpwwe2lem11 10684 uniwun 10783 tskr1om2 10811 tskuni 10826 axgroth3 10874 inaprc 10879 tskmval 10882 tskmcl 10884 suplem1pr 11095 lbsextlem2 21140 lbsextlem3 21141 isbasis3g 22943 eltg2b 22953 tgcl 22963 ppttop 23001 epttop 23003 neiptoptop 23126 tgcmp 23396 locfincmp 23521 dissnref 23523 comppfsc 23527 1stckgenlem 23548 txuni2 23560 txcmplem1 23636 tgqtop 23707 filuni 23880 alexsubALTlem4 24045 ptcmplem3 24049 ptcmplem4 24050 utoptop 24230 icccmplem1 24829 icccmplem3 24831 cnheibor 24972 bndth 24975 lebnumlem1 24978 bcthlem4 25346 ovolicc2lem5 25541 dyadmbllem 25619 itg2gt0 25781 rexunirn 32420 unipreima 32561 acunirnmpt2 32577 acunirnmpt2f 32578 elrspunidl 33303 ssdifidllem 33331 ssmxidllem 33348 reff 33654 locfinreflem 33655 cmpcref 33665 ddemeas 34069 dya2iocuni 34117 bnj1379 34675 cvmsss2 35102 cvmseu 35104 untuni 35531 dfon2lem3 35609 dfon2lem7 35613 dfon2lem8 35614 brbigcup 35722 neibastop1 36071 neibastop2lem 36072 fvineqsneq 37119 heicant 37356 mblfinlem1 37358 cover2 37416 heiborlem9 37520 unichnidl 37732 erimeq2 38376 prtlem16 38567 prter2 38579 prter3 38580 ssunib 42885 onsupuni 42894 onsuplub 42913 restuni3 44719 disjinfi 44799 cncfuni 45507 intsaluni 45950 salgencntex 45964 |
Copyright terms: Public domain | W3C validator |