Theorem elun 3156

Description: Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.)

Assertion

Ref	Expression
elun	⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Proof of Theorem elun

Dummy variable 𝑥 is distinct from all other variables.

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 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

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