Theorem elun 3288

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 2760	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2760	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2760	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 717	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2250	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2250	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 794	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3145	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2896	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 705	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 105   ∨ wo 709   = wceq 1363   ∈ wcel 2158  Vcvv 2749   ∪ cun 3139

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-un 3145

This theorem is referenced by:  uneqri  3289  uncom  3291  uneq1  3294  unass  3304  ssun1  3310  unss1  3316  ssequn1  3317  unss  3321  rexun  3327  ralunb  3328  unssdif  3382  unssin  3386  inssun  3387  indi  3394  undi  3395  difundi  3399  difindiss  3401  undif3ss  3408  symdifxor  3413  rabun2  3426  reuun2  3430  undif4  3497  ssundifim  3518  dcun  3545  dfpr2  3623  eltpg  3649  pwprss  3817  pwtpss  3818  uniun  3840  intun  3887  iunun  3977  iunxun  3978  iinuniss  3981  brun  4066  undifexmid  4205  exmidundif  4218  exmidundifim  4219  exmid1stab  4220  pwunss  4295  elsuci  4415  elsucg  4416  elsuc2g  4417  ordsucim  4511  sucprcreg  4560  opthprc  4689  xpundi  4694  xpundir  4695  funun  5272  mptun  5359  unpreima  5654  reldmtpos  6268  dftpos4  6278  tpostpos  6279  onunsnss  6930  unfidisj  6935  undifdcss  6936  fidcenumlemrks  6966  djulclb  7068  eldju  7081  eldju2ndl  7085  eldju2ndr  7086  ctssdccl  7124  pw1nel3  7244  sucpw1nel3  7246  elnn0  9192  un0addcl  9223  un0mulcl  9224  elxnn0  9255  ltxr  9789  elxr  9790  fzsplit2  10064  elfzp1  10086  uzsplit  10106  elfzp12  10113  fz01or  10125  fzosplit  10191  fzouzsplit  10193  elfzonlteqm1  10224  fzosplitsni  10249  hashinfuni  10771  hashennnuni  10773  hashunlem  10798  zfz1isolemiso  10833  summodclem3  11402  fsumsplit  11429  fsumsplitsn  11432  sumsplitdc  11454  fprodsplitdc  11618  fprodsplit  11619  fprodunsn  11626  fprodsplitsn  11655  nnnn0modprm0  12269  prm23lt5  12277  reopnap  14391  lgsdir2  14787  2lgsoddprmlem3  14812  djulclALT  14906  djurclALT  14907  bj-charfun  14912  bj-nntrans  15056  bj-nnelirr  15058