Theorem elun 3362

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 2827	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2827	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2827	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 724	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2297	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2297	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 801	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3217	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2966	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 712	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 105   ∨ wo 716   = wceq 1398   ∈ wcel 2205  Vcvv 2815   ∪ cun 3211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217

This theorem is referenced by:  uneqri  3363  uncom  3365  uneq1  3368  unass  3378  ssun1  3384  unss1  3390  ssequn1  3391  unss  3395  rexun  3401  ralunb  3402  unssdif  3458  unssin  3462  inssun  3463  indi  3470  undi  3471  difundi  3475  difindiss  3477  undif3ss  3484  symdifxor  3489  rabun2  3502  reuun2  3506  undif4  3573  ssundifim  3595  dcun  3621  dfpr2  3710  eltpg  3736  pwprss  3912  pwtpss  3913  uniun  3935  intun  3982  iunun  4072  iunxun  4073  iinuniss  4076  brun  4163  undifexmid  4308  exmidundif  4321  exmidundifim  4322  exmid1stab  4323  pwunss  4406  elsuci  4526  elsucg  4527  elsuc2g  4528  ordsucim  4624  sucprcreg  4673  opthprc  4803  xpundi  4808  xpundir  4809  funun  5399  mptun  5492  unpreima  5804  reldmtpos  6486  dftpos4  6496  tpostpos  6497  elssdc  7164  onunsnss  7179  unfidisj  7184  undifdcss  7185  fidcenumlemrks  7225  djulclb  7348  eldju  7361  eldju2ndl  7365  eldju2ndr  7366  ctssdccl  7404  pw1nel3  7543  sucpw1nel3  7545  elnn0  9503  un0addcl  9534  un0mulcl  9535  elxnn0  9570  ltxr  10114  elxr  10115  fzsplit2  10390  elfzp1  10413  uzsplit  10433  elfzp12  10440  fz01or  10452  fzosplit  10520  fzouzsplit  10522  elfzonlteqm1  10562  fzosplitsni  10588  hashinfuni  11148  hashennnuni  11150  hashunlem  11176  zfz1isolemiso  11219  ccatrn  11305  cats1un  11421  summodclem3  12074  fsumsplit  12101  fsumsplitsn  12104  sumsplitdc  12126  fprodsplitdc  12290  fprodsplit  12291  fprodunsn  12298  fprodsplitsn  12327  nnnn0modprm0  12961  prm23lt5  12969  reopnap  15460  plyaddlem1  15661  plymullem1  15662  plycoeid3  15671  plycj  15675  lgsdir2  15955  2lgslem3  16023  2lgsoddprmlem3  16033  vtxdfifiun  16341  djulclALT  16622  djurclALT  16623  bj-charfun  16626  bj-nntrans  16770  bj-nnelirr  16772