![]() |
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 | ⊢ (A ∈ (B ∪ 𝐶) ↔ (A ∈ B ∨ A ∈ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2560 | . 2 ⊢ (A ∈ (B ∪ 𝐶) → A ∈ V) | |
2 | elex 2560 | . . 3 ⊢ (A ∈ B → A ∈ V) | |
3 | elex 2560 | . . 3 ⊢ (A ∈ 𝐶 → A ∈ V) | |
4 | 2, 3 | jaoi 635 | . 2 ⊢ ((A ∈ B ∨ A ∈ 𝐶) → A ∈ V) |
5 | eleq1 2097 | . . . 4 ⊢ (x = A → (x ∈ B ↔ A ∈ B)) | |
6 | eleq1 2097 | . . . 4 ⊢ (x = A → (x ∈ 𝐶 ↔ A ∈ 𝐶)) | |
7 | 5, 6 | orbi12d 706 | . . 3 ⊢ (x = A → ((x ∈ B ∨ x ∈ 𝐶) ↔ (A ∈ B ∨ A ∈ 𝐶))) |
8 | df-un 2916 | . . 3 ⊢ (B ∪ 𝐶) = {x ∣ (x ∈ B ∨ x ∈ 𝐶)} | |
9 | 7, 8 | elab2g 2683 | . 2 ⊢ (A ∈ V → (A ∈ (B ∪ 𝐶) ↔ (A ∈ B ∨ A ∈ 𝐶))) |
10 | 1, 4, 9 | pm5.21nii 619 | 1 ⊢ (A ∈ (B ∪ 𝐶) ↔ (A ∈ B ∨ A ∈ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ∨ wo 628 = wceq 1242 ∈ wcel 1390 Vcvv 2551 ∪ cun 2909 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bndl 1396 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-tru 1245 df-nf 1347 df-sb 1643 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-v 2553 df-un 2916 |
This theorem is referenced by: uneqri 3079 uncom 3081 uneq1 3084 unass 3094 ssun1 3100 unss1 3106 ssequn1 3107 unss 3111 rexun 3117 ralunb 3118 unssdif 3166 unssin 3170 inssun 3171 indi 3178 undi 3179 difundi 3183 difindiss 3185 undif3ss 3192 symdifxor 3197 rabun2 3210 reuun2 3214 undif4 3278 ssundifim 3300 dfpr2 3383 eltpg 3407 pwprss 3567 pwtpss 3568 uniun 3590 intun 3637 iunun 3725 iunxun 3726 iinuniss 3728 brun 3801 pwunss 4011 elsuci 4106 elsucg 4107 elsuc2g 4108 ordsucim 4192 sucprcreg 4227 opthprc 4334 xpundi 4339 xpundir 4340 funun 4887 mptun 4972 unpreima 5235 reldmtpos 5809 dftpos4 5819 tpostpos 5820 elnn0 7959 un0addcl 7991 un0mulcl 7992 ltxr 8465 elxr 8466 fzsplit2 8684 elfzp1 8704 uzsplit 8724 elfzp12 8731 fzosplit 8803 fzouzsplit 8805 elfzonlteqm1 8836 fzosplitsni 8861 bj-nntrans 9411 bj-nnelirr 9413 |
Copyright terms: Public domain | W3C validator |