![]() |
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 2823 | . . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵)) | |
2 | eleq1 2822 | . . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | |
3 | 1, 2 | anbi12d 632 | . . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶))) |
4 | 3 | spcegv 3586 | . . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))) |
5 | 4 | anabsi7 670 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)) |
6 | eluni 4907 | . 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)) | |
7 | 5, 6 | sylibr 233 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ∪ cuni 4904 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-uni 4905 |
This theorem is referenced by: ssuni 4932 unipw 5446 opeluu 5466 unon 7806 limuni3 7828 uniinqs 8779 trcl 9710 rankwflemb 9775 ac5num 10018 dfac3 10103 isf34lem4 10359 axcclem 10439 ttukeylem7 10497 brdom7disj 10513 brdom6disj 10514 wrdexb 14462 dprdfeq0 19875 tgss2 22459 ppttop 22479 isclo 22560 neips 22586 2ndcomap 22931 2ndcsep 22932 locfincmp 22999 comppfsc 23005 txkgen 23125 txconn 23162 basqtop 23184 nrmr0reg 23222 alexsublem 23517 alexsubALTlem4 23523 alexsubALT 23524 ptcmplem4 23528 unirnblps 23894 unirnbl 23895 blbas 23905 met2ndci 24000 bndth 24443 dyadmbllem 25085 opnmbllem 25087 ssmxidllem 32538 dya2iocnei 33212 dstfrvunirn 33404 pconnconn 34153 cvmcov2 34197 cvmlift2lem11 34235 cvmlift2lem12 34236 neibastop2lem 35150 onint1 35239 icoreunrn 36145 opnmbllem0 36429 heibor1 36584 unichnidl 36805 prtlem16 37645 prter2 37657 naddsuc2 42014 truniALT 43173 unipwrVD 43464 unipwr 43465 truniALTVD 43510 unisnALT 43558 restuni3 43678 disjinfi 43762 stoweidlem43 44632 stoweidlem55 44644 salexct 44923 |
Copyright terms: Public domain | W3C validator |