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 2735 | . 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V) | |
2 | elex 2735 | . . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | elex 2735 | . . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V) | |
4 | 2, 3 | jaoi 706 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V) |
5 | eleq1 2227 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
6 | eleq1 2227 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
7 | 5, 6 | orbi12d 783 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))) |
8 | df-un 3118 | . . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)} | |
9 | 7, 8 | elab2g 2871 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))) |
10 | 1, 4, 9 | pm5.21nii 694 | 1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 698 = wceq 1342 ∈ wcel 2135 Vcvv 2724 ∪ cun 3112 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2726 df-un 3118 |
This theorem is referenced by: uneqri 3262 uncom 3264 uneq1 3267 unass 3277 ssun1 3283 unss1 3289 ssequn1 3290 unss 3294 rexun 3300 ralunb 3301 unssdif 3355 unssin 3359 inssun 3360 indi 3367 undi 3368 difundi 3372 difindiss 3374 undif3ss 3381 symdifxor 3386 rabun2 3399 reuun2 3403 undif4 3469 ssundifim 3490 dcun 3517 dfpr2 3592 eltpg 3618 pwprss 3782 pwtpss 3783 uniun 3805 intun 3852 iunun 3941 iunxun 3942 iinuniss 3945 brun 4030 undifexmid 4169 exmidundif 4182 exmidundifim 4183 pwunss 4258 elsuci 4378 elsucg 4379 elsuc2g 4380 ordsucim 4474 sucprcreg 4523 opthprc 4652 xpundi 4657 xpundir 4658 funun 5229 mptun 5316 unpreima 5607 reldmtpos 6215 dftpos4 6225 tpostpos 6226 onunsnss 6876 unfidisj 6881 undifdcss 6882 fidcenumlemrks 6912 djulclb 7014 eldju 7027 eldju2ndl 7031 eldju2ndr 7032 ctssdccl 7070 pw1nel3 7181 sucpw1nel3 7183 elnn0 9110 un0addcl 9141 un0mulcl 9142 elxnn0 9173 ltxr 9705 elxr 9706 fzsplit2 9979 elfzp1 10001 uzsplit 10021 elfzp12 10028 fz01or 10040 fzosplit 10106 fzouzsplit 10108 elfzonlteqm1 10139 fzosplitsni 10164 hashinfuni 10684 hashennnuni 10686 hashunlem 10711 zfz1isolemiso 10746 summodclem3 11315 fsumsplit 11342 fsumsplitsn 11345 sumsplitdc 11367 fprodsplitdc 11531 fprodsplit 11532 fprodunsn 11539 fprodsplitsn 11568 nnnn0modprm0 12181 prm23lt5 12189 reopnap 13136 djulclALT 13575 djurclALT 13576 bj-charfun 13582 bj-nntrans 13726 bj-nnelirr 13728 exmid1stab 13773 |
Copyright terms: Public domain | W3C validator |