Theorem elun 3305

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 2774	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2774	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2774	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 717	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2259	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2259	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 794	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3161	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2911	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 705	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 105   ∨ wo 709   = wceq 1364   ∈ wcel 2167  Vcvv 2763   ∪ cun 3155

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161

This theorem is referenced by:  uneqri  3306  uncom  3308  uneq1  3311  unass  3321  ssun1  3327  unss1  3333  ssequn1  3334  unss  3338  rexun  3344  ralunb  3345  unssdif  3399  unssin  3403  inssun  3404  indi  3411  undi  3412  difundi  3416  difindiss  3418  undif3ss  3425  symdifxor  3430  rabun2  3443  reuun2  3447  undif4  3514  ssundifim  3535  dcun  3561  dfpr2  3642  eltpg  3668  pwprss  3836  pwtpss  3837  uniun  3859  intun  3906  iunun  3996  iunxun  3997  iinuniss  4000  brun  4085  undifexmid  4227  exmidundif  4240  exmidundifim  4241  exmid1stab  4242  pwunss  4319  elsuci  4439  elsucg  4440  elsuc2g  4441  ordsucim  4537  sucprcreg  4586  opthprc  4715  xpundi  4720  xpundir  4721  funun  5303  mptun  5392  unpreima  5690  reldmtpos  6320  dftpos4  6330  tpostpos  6331  onunsnss  6987  unfidisj  6992  undifdcss  6993  fidcenumlemrks  7028  djulclb  7130  eldju  7143  eldju2ndl  7147  eldju2ndr  7148  ctssdccl  7186  pw1nel3  7316  sucpw1nel3  7318  elnn0  9270  un0addcl  9301  un0mulcl  9302  elxnn0  9333  ltxr  9869  elxr  9870  fzsplit2  10144  elfzp1  10166  uzsplit  10186  elfzp12  10193  fz01or  10205  fzosplit  10272  fzouzsplit  10274  elfzonlteqm1  10305  fzosplitsni  10330  hashinfuni  10888  hashennnuni  10890  hashunlem  10915  zfz1isolemiso  10950  summodclem3  11564  fsumsplit  11591  fsumsplitsn  11594  sumsplitdc  11616  fprodsplitdc  11780  fprodsplit  11781  fprodunsn  11788  fprodsplitsn  11817  nnnn0modprm0  12451  prm23lt5  12459  reopnap  14868  plyaddlem1  15069  plymullem1  15070  plycoeid3  15079  plycj  15083  lgsdir2  15360  2lgslem3  15428  2lgsoddprmlem3  15438  djulclALT  15533  djurclALT  15534  bj-charfun  15539  bj-nntrans  15683  bj-nnelirr  15685