Theorem elun 3370

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 2833	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2833	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2833	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 728	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2301	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2301	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 805	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3224	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2973	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 716	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 105   ∨ wo 720   = wceq 1402   ∈ wcel 2209  Vcvv 2821   ∪ cun 3218

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224

This theorem is referenced by:  uneqri  3371  uncom  3373  uneq1  3376  unass  3386  ssun1  3392  unss1  3398  ssequn1  3399  unss  3403  rexun  3409  ralunb  3410  unssdif  3466  unssin  3470  inssun  3471  indi  3478  undi  3479  difundi  3483  difindiss  3485  undif3ss  3492  symdifxor  3497  rabun2  3512  reuun2  3516  undif4  3587  ssundifim  3611  dcun  3637  dfpr2  3727  eltpg  3753  pwprss  3929  pwtpss  3930  uniun  3952  intun  3999  iunun  4089  iunxun  4090  iinuniss  4093  brun  4180  undifexmid  4328  exmidundif  4341  exmidundifim  4342  exmid1stab  4343  pwunss  4426  elsuci  4546  elsucg  4547  elsuc2g  4548  ordsucim  4645  sucprcreg  4694  opthprc  4824  xpundi  4829  xpundir  4830  funun  5420  mptun  5513  unpreima  5827  reldmtpos  6518  dftpos4  6528  tpostpos  6529  elssdc  7203  onunsnss  7218  unfidisj  7223  undifdcss  7224  fidcenumlemrks  7264  djulclb  7389  eldju  7402  eldju2ndl  7406  eldju2ndr  7407  ctssdccl  7445  pw1nel3  7584  sucpw1nel3  7586  elnn0  9548  un0addcl  9579  un0mulcl  9580  elxnn0  9615  ltxr  10160  elxr  10161  fzsplit2  10438  fzsplit3  10441  elfzp1  10462  uzsplit  10482  elfzp12  10489  fz01or  10501  fzosplit  10569  fzouzsplit  10571  elfzonlteqm1  10611  fzosplitsni  10637  hashinfuni  11199  hashennnuni  11201  hashunlem  11227  hashf1lem2  11269  zfz1isolemiso  11274  ccatrn  11360  cats1un  11476  summodclem3  12130  fsumsplit  12157  fsumsplitsn  12160  sumsplitdc  12182  fprodsplitdc  12346  fprodsplit  12347  fprodunsn  12354  fprodsplitsn  12383  nnnn0modprm0  13017  prm23lt5  13025  gsumfsum  14906  reopnap  15630  plyaddlem1  15831  plymullem1  15832  plycoeid3  15841  plycj  15845  lgsdir2  16135  2lgslem3  16203  2lgsoddprmlem3  16213  vtxdfifiun  16521  djulclALT  16812  djurclALT  16813  bj-charfun  16816  bj-nntrans  16960  bj-nnelirr  16962