Theorem elun 3346

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 2812	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2812	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2812	. . 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 3202	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2951	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 709	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

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

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 2802  df-un 3202

This theorem is referenced by:  uneqri  3347  uncom  3349  uneq1  3352  unass  3362  ssun1  3368  unss1  3374  ssequn1  3375  unss  3379  rexun  3385  ralunb  3386  unssdif  3440  unssin  3444  inssun  3445  indi  3452  undi  3453  difundi  3457  difindiss  3459  undif3ss  3466  symdifxor  3471  rabun2  3484  reuun2  3488  undif4  3555  ssundifim  3576  dcun  3602  dfpr2  3686  eltpg  3712  pwprss  3887  pwtpss  3888  uniun  3910  intun  3957  iunun  4047  iunxun  4048  iinuniss  4051  brun  4138  undifexmid  4281  exmidundif  4294  exmidundifim  4295  exmid1stab  4296  pwunss  4378  elsuci  4498  elsucg  4499  elsuc2g  4500  ordsucim  4596  sucprcreg  4645  opthprc  4775  xpundi  4780  xpundir  4781  funun  5368  mptun  5461  unpreima  5768  reldmtpos  6414  dftpos4  6424  tpostpos  6425  elssdc  7089  onunsnss  7104  unfidisj  7109  undifdcss  7110  fidcenumlemrks  7146  djulclb  7248  eldju  7261  eldju2ndl  7265  eldju2ndr  7266  ctssdccl  7304  pw1nel3  7442  sucpw1nel3  7444  elnn0  9397  un0addcl  9428  un0mulcl  9429  elxnn0  9460  ltxr  10003  elxr  10004  fzsplit2  10278  elfzp1  10300  uzsplit  10320  elfzp12  10327  fz01or  10339  fzosplit  10407  fzouzsplit  10409  elfzonlteqm1  10448  fzosplitsni  10474  hashinfuni  11032  hashennnuni  11034  hashunlem  11060  zfz1isolemiso  11096  ccatrn  11179  cats1un  11295  summodclem3  11934  fsumsplit  11961  fsumsplitsn  11964  sumsplitdc  11986  fprodsplitdc  12150  fprodsplit  12151  fprodunsn  12158  fprodsplitsn  12187  nnnn0modprm0  12821  prm23lt5  12829  reopnap  15263  plyaddlem1  15464  plymullem1  15465  plycoeid3  15474  plycj  15478  lgsdir2  15755  2lgslem3  15823  2lgsoddprmlem3  15833  vtxdfifiun  16108  djulclALT  16347  djurclALT  16348  bj-charfun  16352  bj-nntrans  16496  bj-nnelirr  16498