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 1852 | . 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥)) | |
2 | eluni 4833 | . 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) | |
3 | df-rex 3141 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥)) | |
4 | 1, 2, 3 | 3bitr4i 304 | 1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 ∃wex 1771 ∈ wcel 2105 ∃wrex 3136 ∪ cuni 4830 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rex 3141 df-v 3494 df-uni 4831 |
This theorem is referenced by: uni0b 4855 intssuni 4889 iuncom4 4918 inuni 5237 cnvuni 5750 chfnrn 6811 ssorduni 7489 unon 7535 limuni3 7556 onfununi 7967 oarec 8177 uniinqs 8366 fissuni 8817 finsschain 8819 r1sdom 9191 rankuni2b 9270 cflm 9660 coflim 9671 axdc3lem2 9861 fpwwe2lem12 10051 uniwun 10150 tskr1om2 10178 tskuni 10193 axgroth3 10241 inaprc 10246 tskmval 10249 tskmcl 10251 suplem1pr 10462 lbsextlem2 19860 lbsextlem3 19861 isbasis3g 21485 eltg2b 21495 tgcl 21505 ppttop 21543 epttop 21545 neiptoptop 21667 tgcmp 21937 locfincmp 22062 dissnref 22064 comppfsc 22068 1stckgenlem 22089 txuni2 22101 txcmplem1 22177 tgqtop 22248 filuni 22421 alexsubALTlem4 22586 ptcmplem3 22590 ptcmplem4 22591 utoptop 22770 icccmplem1 23357 icccmplem3 23359 cnheibor 23486 bndth 23489 lebnumlem1 23492 bcthlem4 23857 ovolicc2lem5 24049 dyadmbllem 24127 itg2gt0 24288 rexunirn 30183 unipreima 30319 acunirnmpt2 30333 acunirnmpt2f 30334 reff 31002 locfinreflem 31003 cmpcref 31013 ddemeas 31394 dya2iocuni 31440 bnj1379 32001 cvmsss2 32418 cvmseu 32420 untuni 32832 dfon2lem3 32927 dfon2lem7 32931 dfon2lem8 32932 frrlem9 33028 brbigcup 33256 neibastop1 33604 neibastop2lem 33605 fvineqsneq 34575 heicant 34808 mblfinlem1 34810 cover2 34870 heiborlem9 34978 unichnidl 35190 erim2 35791 prtlem16 35885 prter2 35897 prter3 35898 restuni3 41261 disjinfi 41330 cncfuni 42045 intsaluni 42489 salgencntex 42503 |
Copyright terms: Public domain | W3C validator |