Theorem elun 3084

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 2566	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2566	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2566	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 636	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2100	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2100	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 707	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 2922	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2689	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 620	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 98   ∨ wo 629   = wceq 1243   ∈ wcel 1393  Vcvv 2557   ∪ cun 2915

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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922

This theorem is referenced by:  uneqri  3085  uncom  3087  uneq1  3090  unass  3100  ssun1  3106  unss1  3112  ssequn1  3113  unss  3117  rexun  3123  ralunb  3124  unssdif  3172  unssin  3176  inssun  3177  indi  3184  undi  3185  difundi  3189  difindiss  3191  undif3ss  3198  symdifxor  3203  rabun2  3216  reuun2  3220  undif4  3284  ssundifim  3306  dfpr2  3394  eltpg  3416  pwprss  3576  pwtpss  3577  uniun  3599  intun  3646  iunun  3734  iunxun  3735  iinuniss  3737  brun  3810  pwunss  4020  elsuci  4140  elsucg  4141  elsuc2g  4142  ordsucim  4226  sucprcreg  4273  opthprc  4391  xpundi  4396  xpundir  4397  funun  4944  mptun  5029  unpreima  5292  reldmtpos  5868  dftpos4  5878  tpostpos  5879  onunsnss  6355  elnn0  8183  un0addcl  8215  un0mulcl  8216  ltxr  8695  elxr  8696  fzsplit2  8914  elfzp1  8934  uzsplit  8954  elfzp12  8961  fzosplit  9033  fzouzsplit  9035  elfzonlteqm1  9066  fzosplitsni  9091  bj-nntrans  10076  bj-nnelirr  10078