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 2690 | . . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵)) | |
2 | eleq1 2689 | . . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | |
3 | 1, 2 | anbi12d 747 | . . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶))) |
4 | 3 | spcegv 3294 | . . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))) |
5 | 4 | anabsi7 860 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)) |
6 | eluni 4439 | . 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)) | |
7 | 5, 6 | sylibr 224 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∃wex 1704 ∈ wcel 1990 ∪ cuni 4436 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-uni 4437 |
This theorem is referenced by: ssuni 4459 ssuniOLD 4460 unipw 4918 opeluu 4939 unon 7031 limuni3 7052 uniinqs 7827 trcl 8604 rankwflemb 8656 ac5num 8859 dfac3 8944 isf34lem4 9199 axcclem 9279 ttukeylem7 9337 brdom7disj 9353 brdom6disj 9354 wrdexb 13316 dprdfeq0 18421 tgss2 20791 ppttop 20811 isclo 20891 neips 20917 2ndcomap 21261 2ndcsep 21262 locfincmp 21329 comppfsc 21335 txkgen 21455 txconn 21492 basqtop 21514 nrmr0reg 21552 alexsublem 21848 alexsubALTlem4 21854 alexsubALT 21855 ptcmplem4 21859 unirnblps 22224 unirnbl 22225 blbas 22235 met2ndci 22327 bndth 22757 dyadmbllem 23367 opnmbllem 23369 dya2iocnei 30344 dstfrvunirn 30536 pconnconn 31213 cvmcov2 31257 cvmlift2lem11 31295 cvmlift2lem12 31296 neibastop2lem 32355 onint1 32448 icoreunrn 33207 opnmbllem0 33445 heibor1 33609 unichnidl 33830 prtlem16 34154 prter2 34166 truniALT 38751 unipwrVD 39067 unipwr 39068 truniALTVD 39114 unisnALT 39162 restuni3 39301 disjinfi 39380 stoweidlem43 40260 stoweidlem55 40272 salexct 40552 |
Copyright terms: Public domain | W3C validator |