![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elun | GIF version |
Description: Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.) |
Ref | Expression |
---|---|
elun | ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2760 | . 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V) | |
2 | elex 2760 | . . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | elex 2760 | . . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V) | |
4 | 2, 3 | jaoi 717 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V) |
5 | eleq1 2250 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
6 | eleq1 2250 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
7 | 5, 6 | orbi12d 794 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))) |
8 | df-un 3145 | . . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)} | |
9 | 7, 8 | elab2g 2896 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))) |
10 | 1, 4, 9 | pm5.21nii 705 | 1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∨ wo 709 = wceq 1363 ∈ wcel 2158 Vcvv 2749 ∪ cun 3139 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-v 2751 df-un 3145 |
This theorem is referenced by: uneqri 3289 uncom 3291 uneq1 3294 unass 3304 ssun1 3310 unss1 3316 ssequn1 3317 unss 3321 rexun 3327 ralunb 3328 unssdif 3382 unssin 3386 inssun 3387 indi 3394 undi 3395 difundi 3399 difindiss 3401 undif3ss 3408 symdifxor 3413 rabun2 3426 reuun2 3430 undif4 3497 ssundifim 3518 dcun 3545 dfpr2 3623 eltpg 3649 pwprss 3817 pwtpss 3818 uniun 3840 intun 3887 iunun 3977 iunxun 3978 iinuniss 3981 brun 4066 undifexmid 4205 exmidundif 4218 exmidundifim 4219 exmid1stab 4220 pwunss 4295 elsuci 4415 elsucg 4416 elsuc2g 4417 ordsucim 4511 sucprcreg 4560 opthprc 4689 xpundi 4694 xpundir 4695 funun 5272 mptun 5359 unpreima 5654 reldmtpos 6268 dftpos4 6278 tpostpos 6279 onunsnss 6930 unfidisj 6935 undifdcss 6936 fidcenumlemrks 6966 djulclb 7068 eldju 7081 eldju2ndl 7085 eldju2ndr 7086 ctssdccl 7124 pw1nel3 7244 sucpw1nel3 7246 elnn0 9192 un0addcl 9223 un0mulcl 9224 elxnn0 9255 ltxr 9789 elxr 9790 fzsplit2 10064 elfzp1 10086 uzsplit 10106 elfzp12 10113 fz01or 10125 fzosplit 10191 fzouzsplit 10193 elfzonlteqm1 10224 fzosplitsni 10249 hashinfuni 10771 hashennnuni 10773 hashunlem 10798 zfz1isolemiso 10833 summodclem3 11402 fsumsplit 11429 fsumsplitsn 11432 sumsplitdc 11454 fprodsplitdc 11618 fprodsplit 11619 fprodunsn 11626 fprodsplitsn 11655 nnnn0modprm0 12269 prm23lt5 12277 reopnap 14391 lgsdir2 14787 2lgsoddprmlem3 14812 djulclALT 14906 djurclALT 14907 bj-charfun 14912 bj-nntrans 15056 bj-nnelirr 15058 |
Copyright terms: Public domain | W3C validator |