Theorem elun 3262

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 2736	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2736	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2736	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 706	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2228	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2228	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 783	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3119	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2872	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 694	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 104   ∨ wo 698   = wceq 1343   ∈ wcel 2136  Vcvv 2725   ∪ cun 3113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-un 3119

This theorem is referenced by:  uneqri  3263  uncom  3265  uneq1  3268  unass  3278  ssun1  3284  unss1  3290  ssequn1  3291  unss  3295  rexun  3301  ralunb  3302  unssdif  3356  unssin  3360  inssun  3361  indi  3368  undi  3369  difundi  3373  difindiss  3375  undif3ss  3382  symdifxor  3387  rabun2  3400  reuun2  3404  undif4  3470  ssundifim  3491  dcun  3518  dfpr2  3594  eltpg  3620  pwprss  3784  pwtpss  3785  uniun  3807  intun  3854  iunun  3943  iunxun  3944  iinuniss  3947  brun  4032  undifexmid  4171  exmidundif  4184  exmidundifim  4185  pwunss  4260  elsuci  4380  elsucg  4381  elsuc2g  4382  ordsucim  4476  sucprcreg  4525  opthprc  4654  xpundi  4659  xpundir  4660  funun  5231  mptun  5318  unpreima  5609  reldmtpos  6217  dftpos4  6227  tpostpos  6228  onunsnss  6878  unfidisj  6883  undifdcss  6884  fidcenumlemrks  6914  djulclb  7016  eldju  7029  eldju2ndl  7033  eldju2ndr  7034  ctssdccl  7072  pw1nel3  7183  sucpw1nel3  7185  elnn0  9112  un0addcl  9143  un0mulcl  9144  elxnn0  9175  ltxr  9707  elxr  9708  fzsplit2  9981  elfzp1  10003  uzsplit  10023  elfzp12  10030  fz01or  10042  fzosplit  10108  fzouzsplit  10110  elfzonlteqm1  10141  fzosplitsni  10166  hashinfuni  10686  hashennnuni  10688  hashunlem  10713  zfz1isolemiso  10748  summodclem3  11317  fsumsplit  11344  fsumsplitsn  11347  sumsplitdc  11369  fprodsplitdc  11533  fprodsplit  11534  fprodunsn  11541  fprodsplitsn  11570  nnnn0modprm0  12183  prm23lt5  12191  reopnap  13138  lgsdir2  13534  djulclALT  13642  djurclALT  13643  bj-charfun  13649  bj-nntrans  13793  bj-nnelirr  13795  exmid1stab  13840