![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elunii | Structured version Visualization version GIF version |
Description: Membership in class union. (Contributed by NM, 24-Mar-1995.) |
Ref | Expression |
---|---|
elunii | ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 2828 | . . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵)) | |
2 | eleq1 2827 | . . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | |
3 | 1, 2 | anbi12d 749 | . . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶))) |
4 | 3 | spcegv 3434 | . . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))) |
5 | 4 | anabsi7 895 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)) |
6 | eluni 4591 | . 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)) | |
7 | 5, 6 | sylibr 224 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1632 ∃wex 1853 ∈ wcel 2139 ∪ cuni 4588 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-v 3342 df-uni 4589 |
This theorem is referenced by: ssuni 4611 ssuniOLD 4612 unipw 5067 opeluu 5087 unon 7196 limuni3 7217 uniinqs 7994 trcl 8777 rankwflemb 8829 ac5num 9049 dfac3 9134 isf34lem4 9391 axcclem 9471 ttukeylem7 9529 brdom7disj 9545 brdom6disj 9546 wrdexb 13502 dprdfeq0 18621 tgss2 20993 ppttop 21013 isclo 21093 neips 21119 2ndcomap 21463 2ndcsep 21464 locfincmp 21531 comppfsc 21537 txkgen 21657 txconn 21694 basqtop 21716 nrmr0reg 21754 alexsublem 22049 alexsubALTlem4 22055 alexsubALT 22056 ptcmplem4 22060 unirnblps 22425 unirnbl 22426 blbas 22436 met2ndci 22528 bndth 22958 dyadmbllem 23567 opnmbllem 23569 dya2iocnei 30653 dstfrvunirn 30845 pconnconn 31520 cvmcov2 31564 cvmlift2lem11 31602 cvmlift2lem12 31603 neibastop2lem 32661 onint1 32754 icoreunrn 33518 cnfin0 33551 opnmbllem0 33758 heibor1 33922 unichnidl 34143 prtlem16 34658 prter2 34670 truniALT 39253 unipwrVD 39566 unipwr 39567 truniALTVD 39613 unisnALT 39661 restuni3 39800 disjinfi 39879 stoweidlem43 40763 stoweidlem55 40775 salexct 41055 |
Copyright terms: Public domain | W3C validator |