![]() |
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 2644 | . 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V) | |
2 | elex 2644 | . . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | elex 2644 | . . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V) | |
4 | 2, 3 | jaoi 674 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V) |
5 | eleq1 2157 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
6 | eleq1 2157 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
7 | 5, 6 | orbi12d 745 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))) |
8 | df-un 3017 | . . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)} | |
9 | 7, 8 | elab2g 2776 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))) |
10 | 1, 4, 9 | pm5.21nii 658 | 1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 667 = wceq 1296 ∈ wcel 1445 Vcvv 2633 ∪ cun 3011 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 df-un 3017 |
This theorem is referenced by: uneqri 3157 uncom 3159 uneq1 3162 unass 3172 ssun1 3178 unss1 3184 ssequn1 3185 unss 3189 rexun 3195 ralunb 3196 unssdif 3250 unssin 3254 inssun 3255 indi 3262 undi 3263 difundi 3267 difindiss 3269 undif3ss 3276 symdifxor 3281 rabun2 3294 reuun2 3298 undif4 3364 ssundifim 3385 dcun 3412 dfpr2 3485 eltpg 3508 pwprss 3671 pwtpss 3672 uniun 3694 intun 3741 iunun 3830 iunxun 3831 iinuniss 3833 brun 3913 undifexmid 4049 exmidundif 4058 exmidundifim 4059 pwunss 4134 elsuci 4254 elsucg 4255 elsuc2g 4256 ordsucim 4345 sucprcreg 4393 opthprc 4518 xpundi 4523 xpundir 4524 funun 5092 mptun 5178 unpreima 5463 reldmtpos 6056 dftpos4 6066 tpostpos 6067 onunsnss 6707 unfidisj 6712 undifdcss 6713 fidcenumlemrks 6742 djulclb 6827 djur 6837 eldju 6839 djuun 6840 eldju2ndl 6843 eldju2ndr 6844 elnn0 8773 un0addcl 8804 un0mulcl 8805 elxnn0 8836 ltxr 9345 elxr 9346 fzsplit2 9613 elfzp1 9635 uzsplit 9655 elfzp12 9662 fz01or 9674 fzosplit 9737 fzouzsplit 9739 elfzonlteqm1 9770 fzosplitsni 9795 hashinfuni 10300 hashennnuni 10302 hashunlem 10327 zfz1isolemiso 10359 summodclem3 10923 fsumsplit 10950 fsumsplitsn 10953 sumsplitdc 10975 djulclALT 12409 djurclALT 12410 bj-nntrans 12554 bj-nnelirr 12556 |
Copyright terms: Public domain | W3C validator |