| 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 2830 | . . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵)) | |
| 2 | eleq1 2829 | . . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | |
| 3 | 1, 2 | anbi12d 632 | . . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶))) |
| 4 | 3 | spcegv 3597 | . . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))) |
| 5 | 4 | anabsi7 671 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)) |
| 6 | eluni 4910 | . 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)) | |
| 7 | 5, 6 | sylibr 234 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2108 ∪ 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-v 3482 df-uni 4908 |
| This theorem is referenced by: ssuni 4932 unipw 5455 opeluu 5475 unon 7851 limuni3 7873 naddsuc2 8739 uniinqs 8837 trcl 9768 rankwflemb 9833 ac5num 10076 dfac3 10161 isf34lem4 10417 axcclem 10497 ttukeylem7 10555 brdom7disj 10571 brdom6disj 10572 wrdexb 14563 dprdfeq0 20042 tgss2 22994 ppttop 23014 isclo 23095 neips 23121 2ndcomap 23466 2ndcsep 23467 locfincmp 23534 comppfsc 23540 txkgen 23660 txconn 23697 basqtop 23719 nrmr0reg 23757 alexsublem 24052 alexsubALTlem4 24058 alexsubALT 24059 ptcmplem4 24063 unirnblps 24429 unirnbl 24430 blbas 24440 met2ndci 24535 bndth 24990 dyadmbllem 25634 opnmbllem 25636 ssdifidllem 33484 ssmxidllem 33501 dya2iocnei 34284 dstfrvunirn 34477 pconnconn 35236 cvmcov2 35280 cvmlift2lem11 35318 cvmlift2lem12 35319 neibastop2lem 36361 onint1 36450 icoreunrn 37360 opnmbllem0 37663 heibor1 37817 unichnidl 38038 prtlem16 38870 prter2 38882 truniALT 44561 unipwrVD 44852 unipwr 44853 truniALTVD 44898 unisnALT 44946 restuni3 45123 disjinfi 45197 stoweidlem43 46058 stoweidlem55 46070 salexct 46349 |
| Copyright terms: Public domain | W3C validator |