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  7314  sucpw1nel3  7316  elnn0  9268  un0addcl  9299  un0mulcl  9300  elxnn0  9331  ltxr  9867  elxr  9868  fzsplit2  10142  elfzp1  10164  uzsplit  10184  elfzp12  10191  fz01or  10203  fzosplit  10270  fzouzsplit  10272  elfzonlteqm1  10303  fzosplitsni  10328  hashinfuni  10886  hashennnuni  10888  hashunlem  10913  zfz1isolemiso  10948  summodclem3  11562  fsumsplit  11589  fsumsplitsn  11592  sumsplitdc  11614  fprodsplitdc  11778  fprodsplit  11779  fprodunsn  11786  fprodsplitsn  11815  nnnn0modprm0  12449  prm23lt5  12457  reopnap  14866  plyaddlem1  15067  plymullem1  15068  plycoeid3  15077  plycj  15081  lgsdir2  15358  2lgslem3  15426  2lgsoddprmlem3  15436  djulclALT  15531  djurclALT  15532  bj-charfun  15537  bj-nntrans  15681  bj-nnelirr  15683