| 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 1861 | . 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥)) | |
| 2 | eluni 4910 | . 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) | |
| 3 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥)) | |
| 4 | 1, 2, 3 | 3bitr4i 303 | 1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1779 ∈ wcel 2108 ∃wrex 3070 ∪ cuni 4907 |
| 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 |
| 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-rex 3071 df-v 3482 df-uni 4908 |
| This theorem is referenced by: uni0b 4933 intssuni 4970 iuncom4 5000 inuni 5350 cnvuni 5897 chfnrn 7069 ssorduni 7799 unon 7851 limuni3 7873 frrlem9 8319 onfununi 8381 oarec 8600 uniinqs 8837 fissuni 9397 finsschain 9399 r1sdom 9814 rankuni2b 9893 cflm 10290 coflim 10301 axdc3lem2 10491 fpwwe2lem11 10681 uniwun 10780 tskr1om2 10808 tskuni 10823 axgroth3 10871 inaprc 10876 tskmval 10879 tskmcl 10881 suplem1pr 11092 lbsextlem2 21161 lbsextlem3 21162 isbasis3g 22956 eltg2b 22966 tgcl 22976 ppttop 23014 epttop 23016 neiptoptop 23139 tgcmp 23409 locfincmp 23534 dissnref 23536 comppfsc 23540 1stckgenlem 23561 txuni2 23573 txcmplem1 23649 tgqtop 23720 filuni 23893 alexsubALTlem4 24058 ptcmplem3 24062 ptcmplem4 24063 utoptop 24243 icccmplem1 24844 icccmplem3 24846 cnheibor 24987 bndth 24990 lebnumlem1 24993 bcthlem4 25361 ovolicc2lem5 25556 dyadmbllem 25634 itg2gt0 25795 rexunirn 32511 unipreima 32653 acunirnmpt2 32670 acunirnmpt2f 32671 elrspunidl 33456 ssdifidllem 33484 ssmxidllem 33501 reff 33838 locfinreflem 33839 cmpcref 33849 ddemeas 34237 dya2iocuni 34285 bnj1379 34844 cvmsss2 35279 cvmseu 35281 untuni 35709 dfon2lem3 35786 dfon2lem7 35790 dfon2lem8 35791 brbigcup 35899 neibastop1 36360 neibastop2lem 36361 fvineqsneq 37413 heicant 37662 mblfinlem1 37664 cover2 37722 heiborlem9 37826 unichnidl 38038 erimeq2 38679 prtlem16 38870 prter2 38882 prter3 38883 ssunib 43232 onsupuni 43241 onsuplub 43260 restuni3 45123 disjinfi 45197 cncfuni 45901 intsaluni 46344 salgencntex 46358 |
| Copyright terms: Public domain | W3C validator |