Theorem elun 3221

Description: Membership in union. (Contributed by SF, 10-Jan-2015.)

Assertion

Ref	Expression
elun	⊢ (A ∈ (B ∪ C) ↔ (A ∈ B ∨ A ∈ C))

Proof of Theorem elun

Step	Hyp	Ref	Expression
1		elex 2868	. 2 ⊢ (A ∈ (B ∪ C) → A ∈ V)
2		elex 2868	. . 3 ⊢ (A ∈ B → A ∈ V)
3		elex 2868	. . 3 ⊢ (A ∈ C → A ∈ V)
4	2, 3	jaoi 368	. 2 ⊢ ((A ∈ B ∨ A ∈ C) → A ∈ V)
5		elning 3218	. . . 4 ⊢ (A ∈ V → (A ∈ ( ∼ B ⩃ ∼ C) ↔ (A ∈ ∼ B ⊼ A ∈ ∼ C)))
6		elcomplg 3219	. . . . 5 ⊢ (A ∈ V → (A ∈ ∼ B ↔ ¬ A ∈ B))
7		elcomplg 3219	. . . . 5 ⊢ (A ∈ V → (A ∈ ∼ C ↔ ¬ A ∈ C))
8	6, 7	nanbi12d 1303	. . . 4 ⊢ (A ∈ V → ((A ∈ ∼ B ⊼ A ∈ ∼ C) ↔ (¬ A ∈ B ⊼ ¬ A ∈ C)))
9	5, 8	bitrd 244	. . 3 ⊢ (A ∈ V → (A ∈ ( ∼ B ⩃ ∼ C) ↔ (¬ A ∈ B ⊼ ¬ A ∈ C)))
10		df-un 3215	. . . 4 ⊢ (B ∪ C) = ( ∼ B ⩃ ∼ C)
11	10	eleq2i 2417	. . 3 ⊢ (A ∈ (B ∪ C) ↔ A ∈ ( ∼ B ⩃ ∼ C))
12		oran 482	. . . 4 ⊢ ((A ∈ B ∨ A ∈ C) ↔ ¬ (¬ A ∈ B ∧ ¬ A ∈ C))
13		df-nan 1288	. . . 4 ⊢ ((¬ A ∈ B ⊼ ¬ A ∈ C) ↔ ¬ (¬ A ∈ B ∧ ¬ A ∈ C))
14	12, 13	bitr4i 243	. . 3 ⊢ ((A ∈ B ∨ A ∈ C) ↔ (¬ A ∈ B ⊼ ¬ A ∈ C))
15	9, 11, 14	3bitr4g 279	. 2 ⊢ (A ∈ V → (A ∈ (B ∪ C) ↔ (A ∈ B ∨ A ∈ C)))
16	1, 4, 15	pm5.21nii 342	1 ⊢ (A ∈ (B ∪ C) ↔ (A ∈ B ∨ A ∈ C))

Syntax hints:  ¬ wn 3   ↔ wb 176   ∨ wo 357   ∧ wa 358   ⊼ wnan 1287   ∈ wcel 1710  Vcvv 2860   ⩃ cnin 3205   ∼ ccompl 3206   ∪ cun 3208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-nin 3212  df-compl 3213  df-un 3215

This theorem is referenced by:  elsymdif  3224  uneqri  3407  uncom  3409  uneq1  3412  unass  3421  ssun1  3427  unss1  3433  ssequn1  3434  unss  3438  rexun  3444  ralunb  3445  indi  3502  undi  3503  unineq  3506  undif3  3516  symdif2  3521  rabun2  3535  reuun2  3539  undif4  3608  ssundif  3634  dfpr2  3750  eltpg  3770  pwpr  3884  pwtp  3885  unipr  3906  uniun  3911  intun  3959  iinun2  4033  iunun  4047  iunxun  4048  iinuni  4050  pwadjoin  4120  pw1un  4164  dfimak2  4299  dfaddc2  4382  nnsucelrlem1  4425  nnsucelrlem2  4426  nndisjeq  4430  ltfinex  4465  ltfintrilem1  4466  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenoddnnnul  4515  evenodddisjlem1  4516  nnadjoinlem1  4520  vfinspss  4552  vinf  4556  dfphi2  4570  dfop2lem1  4574  phi011lem1  4599  proj1op  4601  proj2op  4602  eqop  4612  brun  4693  setconslem2  4733  setconslem3  4734  setconslem7  4738  dfswap2  4742  xpundi  4833  xpundir  4834  dmun  4913  funun  5147  unpreima  5409  fvclss  5463  cupex  5817  clos1baseima  5884  connexex  5914  enadjlem1  6060  enadj  6061  enprmaplem4  6080  fce  6189  leconnnc  6219  nmembers1lem3  6271  nncdiv3lem2  6277  nchoicelem6  6295  nchoicelem18  6307