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

This proof depends on syntax axioms:   ↔ wb 105   ∨ wo 720   = wceq 1402   ∈ wcel 2209  Vcvv 2821   ∪ cun 3218

This proof depends on 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 proof 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 used 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  3728  eltpg  3754  pwprss  3931  pwtpss  3932  uniun  3954  intun  4001  iunun  4091  iunxun  4092  iinuniss  4095  brun  4183  undifexmid  4332  exmidundif  4345  exmidundifim  4346  exmid1stab  4347  pwunss  4430  elsuci  4550  elsucg  4551  elsuc2g  4552  ordsucim  4649  sucprcreg  4698  opthprc  4828  xpundi  4833  xpundir  4834  funun  5425  mptun  5518  unpreima  5836  reldmtpos  6529  dftpos4  6539  tpostpos  6540  elssdc  7215  onunsnss  7230  unfidisj  7235  undifdcss  7236  fidcenumlemrks  7277  djulclb  7402  eldju  7415  eldju2ndl  7419  eldju2ndr  7420  ctssdccl  7458  pw1nel3  7597  sucpw1nel3  7599  elnn0  9577  un0addcl  9608  un0mulcl  9609  elxnn0  9642  ltxr  10194  elxr  10195  fzsplit2  10472  fzsplit3  10475  elfzp1  10496  uzsplit  10516  elfzp12  10523  fz01or  10535  fzosplit  10603  fzouzsplit  10605  elfzonlteqm1  10645  fzosplitsni  10671  hashinfuni  11238  hashennnuni  11240  hashunlem  11266  hashf1lem2  11308  zfz1isolemiso  11313  ccatrn  11399  cats1un  11515  summodclem3  12172  fsumsplit  12199  fsumsplitsn  12202  sumsplitdc  12224  fprodsplitdc  12388  fprodsplit  12389  fprodunsn  12396  fprodsplitsn  12425  nnnn0modprm0  13063  prm23lt5  13071  gsummptfidmsplit  14254  gsumunsnfd  14259  gsumfsum  15032  reopnap  15805  plyaddlem1  16006  plymullem1  16007  plycoeid3  16016  plycj  16020  ppinprm  16293  chtnprm  16295  lgsdir2  16390  2lgslem3  16458  2lgsoddprmlem3  16468  vtxdfifiun  16776  djulclALT  17067  djurclALT  17068  bj-charfun  17071  bj-nntrans  17215  bj-nnelirr  17217  idjudju  17285