![]() |
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 1842 | . 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥)) | |
2 | eluni 4748 | . 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) | |
3 | df-rex 3111 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥)) | |
4 | 1, 2, 3 | 3bitr4i 304 | 1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 ∃wex 1761 ∈ wcel 2081 ∃wrex 3106 ∪ cuni 4745 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-rex 3111 df-v 3439 df-uni 4746 |
This theorem is referenced by: uni0b 4770 intssuni 4804 iuncom4 4833 inuni 5137 cnvuni 5643 chfnrn 6684 ssorduni 7356 unon 7402 limuni3 7423 onfununi 7830 oarec 8038 uniinqs 8227 fissuni 8675 finsschain 8677 r1sdom 9049 rankuni2b 9128 cflm 9518 coflim 9529 axdc3lem2 9719 fpwwe2lem12 9909 uniwun 10008 tskr1om2 10036 tskuni 10051 axgroth3 10099 inaprc 10104 tskmval 10107 tskmcl 10109 suplem1pr 10320 lbsextlem2 19621 lbsextlem3 19622 isbasis3g 21241 eltg2b 21251 tgcl 21261 ppttop 21299 epttop 21301 neiptoptop 21423 tgcmp 21693 locfincmp 21818 dissnref 21820 comppfsc 21824 1stckgenlem 21845 txuni2 21857 txcmplem1 21933 tgqtop 22004 filuni 22177 alexsubALTlem4 22342 ptcmplem3 22346 ptcmplem4 22347 utoptop 22526 icccmplem1 23113 icccmplem3 23115 cnheibor 23242 bndth 23245 lebnumlem1 23248 bcthlem4 23613 ovolicc2lem5 23805 dyadmbllem 23883 itg2gt0 24044 rexunirn 29948 unipreima 30081 acunirnmpt2 30095 acunirnmpt2f 30096 reff 30720 locfinreflem 30721 cmpcref 30731 ddemeas 31112 dya2iocuni 31158 bnj1379 31719 cvmsss2 32130 cvmseu 32132 untuni 32544 dfon2lem3 32639 dfon2lem7 32643 dfon2lem8 32644 frrlem9 32741 brbigcup 32969 neibastop1 33317 neibastop2lem 33318 fvineqsneq 34243 heicant 34477 mblfinlem1 34479 cover2 34540 heiborlem9 34648 unichnidl 34860 erim2 35461 prtlem16 35555 prter2 35567 prter3 35568 restuni3 40943 disjinfi 41013 cncfuni 41730 intsaluni 42174 salgencntex 42188 |
Copyright terms: Public domain | W3C validator |