![]() |
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 1827 | . 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥)) | |
2 | eluni 4471 | . 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) | |
3 | df-rex 2947 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥)) | |
4 | 1, 2, 3 | 3bitr4i 292 | 1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 ∃wex 1744 ∈ wcel 2030 ∃wrex 2942 ∪ cuni 4468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rex 2947 df-v 3233 df-uni 4469 |
This theorem is referenced by: uni0b 4495 intssuni 4531 iuncom4 4560 inuni 4856 cnvuni 5341 chfnrn 6368 ssorduni 7027 unon 7073 limuni3 7094 onfununi 7483 oarec 7687 uniinqs 7870 fissuni 8312 finsschain 8314 r1sdom 8675 rankuni2b 8754 cflm 9110 coflim 9121 axdc3lem2 9311 fpwwe2lem12 9501 uniwun 9600 tskr1om2 9628 tskuni 9643 axgroth3 9691 inaprc 9696 tskmval 9699 tskmcl 9701 suplem1pr 9912 lbsextlem2 19207 lbsextlem3 19208 isbasis3g 20801 eltg2b 20811 tgcl 20821 ppttop 20859 epttop 20861 neiptoptop 20983 tgcmp 21252 locfincmp 21377 dissnref 21379 comppfsc 21383 1stckgenlem 21404 txuni2 21416 txcmplem1 21492 tgqtop 21563 filuni 21736 alexsubALTlem4 21901 ptcmplem3 21905 ptcmplem4 21906 utoptop 22085 icccmplem1 22672 icccmplem3 22674 cnheibor 22801 bndth 22804 lebnumlem1 22807 bcthlem4 23170 ovolicc2lem5 23335 dyadmbllem 23413 itg2gt0 23572 rexunirn 29458 unipreima 29574 acunirnmpt2 29588 acunirnmpt2f 29589 reff 30034 locfinreflem 30035 cmpcref 30045 ddemeas 30427 dya2iocuni 30473 bnj1379 31027 cvmsss2 31382 cvmseu 31384 untuni 31712 dfon2lem3 31814 dfon2lem7 31818 dfon2lem8 31819 brbigcup 32130 neibastop1 32479 neibastop2lem 32480 heicant 33574 mblfinlem1 33576 cover2 33638 heiborlem9 33748 unichnidl 33960 prtlem16 34473 prter2 34485 prter3 34486 restuni3 39615 disjinfi 39694 cncfuni 40417 intsaluni 40865 salgencntex 40879 |
Copyright terms: Public domain | W3C validator |