Theorem elun 3345

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 2811	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2811	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2811	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 721	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2292	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2292	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 798	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3201	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2950	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 709	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 105   ∨ wo 713   = wceq 1395   ∈ wcel 2200  Vcvv 2799   ∪ cun 3195

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201

This theorem is referenced by:  uneqri  3346  uncom  3348  uneq1  3351  unass  3361  ssun1  3367  unss1  3373  ssequn1  3374  unss  3378  rexun  3384  ralunb  3385  unssdif  3439  unssin  3443  inssun  3444  indi  3451  undi  3452  difundi  3456  difindiss  3458  undif3ss  3465  symdifxor  3470  rabun2  3483  reuun2  3487  undif4  3554  ssundifim  3575  dcun  3601  dfpr2  3685  eltpg  3711  pwprss  3884  pwtpss  3885  uniun  3907  intun  3954  iunun  4044  iunxun  4045  iinuniss  4048  brun  4135  undifexmid  4277  exmidundif  4290  exmidundifim  4291  exmid1stab  4292  pwunss  4374  elsuci  4494  elsucg  4495  elsuc2g  4496  ordsucim  4592  sucprcreg  4641  opthprc  4770  xpundi  4775  xpundir  4776  funun  5362  mptun  5455  unpreima  5762  reldmtpos  6405  dftpos4  6415  tpostpos  6416  onunsnss  7087  unfidisj  7092  undifdcss  7093  fidcenumlemrks  7128  djulclb  7230  eldju  7243  eldju2ndl  7247  eldju2ndr  7248  ctssdccl  7286  pw1nel3  7424  sucpw1nel3  7426  elnn0  9379  un0addcl  9410  un0mulcl  9411  elxnn0  9442  ltxr  9979  elxr  9980  fzsplit2  10254  elfzp1  10276  uzsplit  10296  elfzp12  10303  fz01or  10315  fzosplit  10383  fzouzsplit  10385  elfzonlteqm1  10424  fzosplitsni  10449  hashinfuni  11007  hashennnuni  11009  hashunlem  11034  zfz1isolemiso  11069  ccatrn  11152  cats1un  11261  summodclem3  11899  fsumsplit  11926  fsumsplitsn  11929  sumsplitdc  11951  fprodsplitdc  12115  fprodsplit  12116  fprodunsn  12123  fprodsplitsn  12152  nnnn0modprm0  12786  prm23lt5  12794  reopnap  15228  plyaddlem1  15429  plymullem1  15430  plycoeid3  15439  plycj  15443  lgsdir2  15720  2lgslem3  15788  2lgsoddprmlem3  15798  djulclALT  16189  djurclALT  16190  bj-charfun  16194  bj-nntrans  16338  bj-nnelirr  16340