Theorem elun 3359

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 2824	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2824	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2824	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 724	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2295	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2295	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 801	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3214	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2963	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 712	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 105   ∨ wo 716   = wceq 1398   ∈ wcel 2203  Vcvv 2812   ∪ cun 3208

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-un 3214

This theorem is referenced by:  uneqri  3360  uncom  3362  uneq1  3365  unass  3375  ssun1  3381  unss1  3387  ssequn1  3388  unss  3392  rexun  3398  ralunb  3399  unssdif  3455  unssin  3459  inssun  3460  indi  3467  undi  3468  difundi  3472  difindiss  3474  undif3ss  3481  symdifxor  3486  rabun2  3499  reuun2  3503  undif4  3570  ssundifim  3592  dcun  3618  dfpr2  3707  eltpg  3733  pwprss  3909  pwtpss  3910  uniun  3932  intun  3979  iunun  4069  iunxun  4070  iinuniss  4073  brun  4160  undifexmid  4305  exmidundif  4318  exmidundifim  4319  exmid1stab  4320  pwunss  4403  elsuci  4523  elsucg  4524  elsuc2g  4525  ordsucim  4621  sucprcreg  4670  opthprc  4800  xpundi  4805  xpundir  4806  funun  5396  mptun  5489  unpreima  5801  reldmtpos  6483  dftpos4  6493  tpostpos  6494  elssdc  7161  onunsnss  7176  unfidisj  7181  undifdcss  7182  fidcenumlemrks  7222  djulclb  7345  eldju  7358  eldju2ndl  7362  eldju2ndr  7363  ctssdccl  7401  pw1nel3  7540  sucpw1nel3  7542  elnn0  9494  un0addcl  9525  un0mulcl  9526  elxnn0  9561  ltxr  10104  elxr  10105  fzsplit2  10380  elfzp1  10402  uzsplit  10422  elfzp12  10429  fz01or  10441  fzosplit  10509  fzouzsplit  10511  elfzonlteqm1  10551  fzosplitsni  10577  hashinfuni  11135  hashennnuni  11137  hashunlem  11163  zfz1isolemiso  11204  ccatrn  11290  cats1un  11406  summodclem3  12059  fsumsplit  12086  fsumsplitsn  12089  sumsplitdc  12111  fprodsplitdc  12275  fprodsplit  12276  fprodunsn  12283  fprodsplitsn  12312  nnnn0modprm0  12946  prm23lt5  12954  reopnap  15398  plyaddlem1  15599  plymullem1  15600  plycoeid3  15609  plycj  15613  lgsdir2  15893  2lgslem3  15961  2lgsoddprmlem3  15971  vtxdfifiun  16279  djulclALT  16560  djurclALT  16561  bj-charfun  16564  bj-nntrans  16708  bj-nnelirr  16710