Theorem elun 3315

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 2784	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2784	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2784	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 718	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2269	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2269	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 795	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3171	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2921	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 706	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 105   ∨ wo 710   = wceq 1373   ∈ wcel 2177  Vcvv 2773   ∪ cun 3165

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3171

This theorem is referenced by:  uneqri  3316  uncom  3318  uneq1  3321  unass  3331  ssun1  3337  unss1  3343  ssequn1  3344  unss  3348  rexun  3354  ralunb  3355  unssdif  3409  unssin  3413  inssun  3414  indi  3421  undi  3422  difundi  3426  difindiss  3428  undif3ss  3435  symdifxor  3440  rabun2  3453  reuun2  3457  undif4  3524  ssundifim  3545  dcun  3571  dfpr2  3653  eltpg  3679  pwprss  3848  pwtpss  3849  uniun  3871  intun  3918  iunun  4008  iunxun  4009  iinuniss  4012  brun  4099  undifexmid  4241  exmidundif  4254  exmidundifim  4255  exmid1stab  4256  pwunss  4334  elsuci  4454  elsucg  4455  elsuc2g  4456  ordsucim  4552  sucprcreg  4601  opthprc  4730  xpundi  4735  xpundir  4736  funun  5320  mptun  5413  unpreima  5712  reldmtpos  6346  dftpos4  6356  tpostpos  6357  onunsnss  7021  unfidisj  7026  undifdcss  7027  fidcenumlemrks  7062  djulclb  7164  eldju  7177  eldju2ndl  7181  eldju2ndr  7182  ctssdccl  7220  pw1nel3  7350  sucpw1nel3  7352  elnn0  9304  un0addcl  9335  un0mulcl  9336  elxnn0  9367  ltxr  9904  elxr  9905  fzsplit2  10179  elfzp1  10201  uzsplit  10221  elfzp12  10228  fz01or  10240  fzosplit  10308  fzouzsplit  10310  elfzonlteqm1  10346  fzosplitsni  10371  hashinfuni  10929  hashennnuni  10931  hashunlem  10956  zfz1isolemiso  10991  ccatrn  11073  summodclem3  11735  fsumsplit  11762  fsumsplitsn  11765  sumsplitdc  11787  fprodsplitdc  11951  fprodsplit  11952  fprodunsn  11959  fprodsplitsn  11988  nnnn0modprm0  12622  prm23lt5  12630  reopnap  15062  plyaddlem1  15263  plymullem1  15264  plycoeid3  15273  plycj  15277  lgsdir2  15554  2lgslem3  15622  2lgsoddprmlem3  15632  djulclALT  15811  djurclALT  15812  bj-charfun  15817  bj-nntrans  15961  bj-nnelirr  15963