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 2826 | . . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵)) | |
2 | eleq1 2825 | . . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | |
3 | 1, 2 | anbi12d 634 | . . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶))) |
4 | 3 | spcegv 3512 | . . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))) |
5 | 4 | anabsi7 671 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)) |
6 | eluni 4822 | . 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)) | |
7 | 5, 6 | sylibr 237 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∃wex 1787 ∈ wcel 2110 ∪ cuni 4819 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-uni 4820 |
This theorem is referenced by: ssuni 4846 unipw 5335 opeluu 5354 unon 7610 limuni3 7631 uniinqs 8479 trcl 9344 rankwflemb 9409 ac5num 9650 dfac3 9735 isf34lem4 9991 axcclem 10071 ttukeylem7 10129 brdom7disj 10145 brdom6disj 10146 wrdexb 14080 dprdfeq0 19409 tgss2 21884 ppttop 21904 isclo 21984 neips 22010 2ndcomap 22355 2ndcsep 22356 locfincmp 22423 comppfsc 22429 txkgen 22549 txconn 22586 basqtop 22608 nrmr0reg 22646 alexsublem 22941 alexsubALTlem4 22947 alexsubALT 22948 ptcmplem4 22952 unirnblps 23317 unirnbl 23318 blbas 23328 met2ndci 23420 bndth 23855 dyadmbllem 24496 opnmbllem 24498 ssmxidllem 31355 dya2iocnei 31961 dstfrvunirn 32153 pconnconn 32906 cvmcov2 32950 cvmlift2lem11 32988 cvmlift2lem12 32989 neibastop2lem 34286 onint1 34375 icoreunrn 35267 opnmbllem0 35550 heibor1 35705 unichnidl 35926 prtlem16 36620 prter2 36632 truniALT 41834 unipwrVD 42125 unipwr 42126 truniALTVD 42171 unisnALT 42219 restuni3 42340 disjinfi 42404 stoweidlem43 43259 stoweidlem55 43271 salexct 43548 |
Copyright terms: Public domain | W3C validator |