Theorem elun 3364

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 2827	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2827	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2827	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 724	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2297	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2297	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 801	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3218	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2967	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 712	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 105   ∨ wo 716   = wceq 1398   ∈ wcel 2205  Vcvv 2815   ∪ cun 3212

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218

This theorem is referenced by:  uneqri  3365  uncom  3367  uneq1  3370  unass  3380  ssun1  3386  unss1  3392  ssequn1  3393  unss  3397  rexun  3403  ralunb  3404  unssdif  3460  unssin  3464  inssun  3465  indi  3472  undi  3473  difundi  3477  difindiss  3479  undif3ss  3486  symdifxor  3491  rabun2  3504  reuun2  3508  undif4  3575  ssundifim  3597  dcun  3623  dfpr2  3713  eltpg  3739  pwprss  3915  pwtpss  3916  uniun  3938  intun  3985  iunun  4075  iunxun  4076  iinuniss  4079  brun  4166  undifexmid  4311  exmidundif  4324  exmidundifim  4325  exmid1stab  4326  pwunss  4409  elsuci  4529  elsucg  4530  elsuc2g  4531  ordsucim  4627  sucprcreg  4676  opthprc  4806  xpundi  4811  xpundir  4812  funun  5402  mptun  5495  unpreima  5807  reldmtpos  6497  dftpos4  6507  tpostpos  6508  elssdc  7175  onunsnss  7190  unfidisj  7195  undifdcss  7196  fidcenumlemrks  7236  djulclb  7359  eldju  7372  eldju2ndl  7376  eldju2ndr  7377  ctssdccl  7415  pw1nel3  7554  sucpw1nel3  7556  elnn0  9518  un0addcl  9549  un0mulcl  9550  elxnn0  9585  ltxr  10130  elxr  10131  fzsplit2  10407  fzsplit3  10410  elfzp1  10431  uzsplit  10451  elfzp12  10458  fz01or  10470  fzosplit  10538  fzouzsplit  10540  elfzonlteqm1  10580  fzosplitsni  10606  hashinfuni  11168  hashennnuni  11170  hashunlem  11196  zfz1isolemiso  11239  ccatrn  11325  cats1un  11441  summodclem3  12094  fsumsplit  12121  fsumsplitsn  12124  sumsplitdc  12146  fprodsplitdc  12310  fprodsplit  12311  fprodunsn  12318  fprodsplitsn  12347  nnnn0modprm0  12981  prm23lt5  12989  reopnap  15540  plyaddlem1  15741  plymullem1  15742  plycoeid3  15751  plycj  15755  lgsdir2  16035  2lgslem3  16103  2lgsoddprmlem3  16113  vtxdfifiun  16421  djulclALT  16712  djurclALT  16713  bj-charfun  16716  bj-nntrans  16860  bj-nnelirr  16862