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  4182  undifexmid  4330  exmidundif  4343  exmidundifim  4344  exmid1stab  4345  pwunss  4428  elsuci  4548  elsucg  4549  elsuc2g  4550  ordsucim  4647  sucprcreg  4696  opthprc  4826  xpundi  4831  xpundir  4832  funun  5422  mptun  5515  unpreima  5833  reldmtpos  6524  dftpos4  6534  tpostpos  6535  elssdc  7209  onunsnss  7224  unfidisj  7229  undifdcss  7230  fidcenumlemrks  7270  djulclb  7396  eldju  7409  eldju2ndl  7413  eldju2ndr  7414  ctssdccl  7452  pw1nel3  7591  sucpw1nel3  7593  elnn0  9570  un0addcl  9601  un0mulcl  9602  elxnn0  9637  ltxr  10188  elxr  10189  fzsplit2  10466  fzsplit3  10469  elfzp1  10490  uzsplit  10510  elfzp12  10517  fz01or  10529  fzosplit  10597  fzouzsplit  10599  elfzonlteqm1  10639  fzosplitsni  10665  hashinfuni  11231  hashennnuni  11233  hashunlem  11259  hashf1lem2  11301  zfz1isolemiso  11306  ccatrn  11392  cats1un  11508  summodclem3  12165  fsumsplit  12192  fsumsplitsn  12195  sumsplitdc  12217  fprodsplitdc  12381  fprodsplit  12382  fprodunsn  12389  fprodsplitsn  12418  nnnn0modprm0  13056  prm23lt5  13064  gsumfsum  14974  reopnap  15699  plyaddlem1  15900  plymullem1  15901  plycoeid3  15910  plycj  15914  ppinprm  16182  chtnprm  16184  lgsdir2  16274  2lgslem3  16342  2lgsoddprmlem3  16352  vtxdfifiun  16660  djulclALT  16951  djurclALT  16952  bj-charfun  16955  bj-nntrans  17099  bj-nnelirr  17101