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  4278  exmidundif  4291  exmidundifim  4292  exmid1stab  4293  pwunss  4375  elsuci  4495  elsucg  4496  elsuc2g  4497  ordsucim  4593  sucprcreg  4642  opthprc  4772  xpundi  4777  xpundir  4778  funun  5365  mptun  5458  unpreima  5765  reldmtpos  6410  dftpos4  6420  tpostpos  6421  elssdc  7080  onunsnss  7095  unfidisj  7100  undifdcss  7101  fidcenumlemrks  7136  djulclb  7238  eldju  7251  eldju2ndl  7255  eldju2ndr  7256  ctssdccl  7294  pw1nel3  7432  sucpw1nel3  7434  elnn0  9387  un0addcl  9418  un0mulcl  9419  elxnn0  9450  ltxr  9988  elxr  9989  fzsplit2  10263  elfzp1  10285  uzsplit  10305  elfzp12  10312  fz01or  10324  fzosplit  10392  fzouzsplit  10394  elfzonlteqm1  10433  fzosplitsni  10458  hashinfuni  11016  hashennnuni  11018  hashunlem  11043  zfz1isolemiso  11079  ccatrn  11162  cats1un  11274  summodclem3  11912  fsumsplit  11939  fsumsplitsn  11942  sumsplitdc  11964  fprodsplitdc  12128  fprodsplit  12129  fprodunsn  12136  fprodsplitsn  12165  nnnn0modprm0  12799  prm23lt5  12807  reopnap  15241  plyaddlem1  15442  plymullem1  15443  plycoeid3  15452  plycj  15456  lgsdir2  15733  2lgslem3  15801  2lgsoddprmlem3  15811  vtxdfifiun  16083  djulclALT  16274  djurclALT  16275  bj-charfun  16279  bj-nntrans  16423  bj-nnelirr  16425