Theorem elun 3304

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

Syntax hints:   ↔ wb 105   ∨ wo 709   = wceq 1364   ∈ wcel 2167  Vcvv 2763   ∪ cun 3155

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161

This theorem is referenced by:  uneqri  3305  uncom  3307  uneq1  3310  unass  3320  ssun1  3326  unss1  3332  ssequn1  3333  unss  3337  rexun  3343  ralunb  3344  unssdif  3398  unssin  3402  inssun  3403  indi  3410  undi  3411  difundi  3415  difindiss  3417  undif3ss  3424  symdifxor  3429  rabun2  3442  reuun2  3446  undif4  3513  ssundifim  3534  dcun  3560  dfpr2  3641  eltpg  3667  pwprss  3835  pwtpss  3836  uniun  3858  intun  3905  iunun  3995  iunxun  3996  iinuniss  3999  brun  4084  undifexmid  4226  exmidundif  4239  exmidundifim  4240  exmid1stab  4241  pwunss  4318  elsuci  4438  elsucg  4439  elsuc2g  4440  ordsucim  4536  sucprcreg  4585  opthprc  4714  xpundi  4719  xpundir  4720  funun  5302  mptun  5389  unpreima  5687  reldmtpos  6311  dftpos4  6321  tpostpos  6322  onunsnss  6978  unfidisj  6983  undifdcss  6984  fidcenumlemrks  7019  djulclb  7121  eldju  7134  eldju2ndl  7138  eldju2ndr  7139  ctssdccl  7177  pw1nel3  7298  sucpw1nel3  7300  elnn0  9251  un0addcl  9282  un0mulcl  9283  elxnn0  9314  ltxr  9850  elxr  9851  fzsplit2  10125  elfzp1  10147  uzsplit  10167  elfzp12  10174  fz01or  10186  fzosplit  10253  fzouzsplit  10255  elfzonlteqm1  10286  fzosplitsni  10311  hashinfuni  10869  hashennnuni  10871  hashunlem  10896  zfz1isolemiso  10931  summodclem3  11545  fsumsplit  11572  fsumsplitsn  11575  sumsplitdc  11597  fprodsplitdc  11761  fprodsplit  11762  fprodunsn  11769  fprodsplitsn  11798  nnnn0modprm0  12424  prm23lt5  12432  reopnap  14782  plyaddlem1  14983  plymullem1  14984  plycoeid3  14993  plycj  14997  lgsdir2  15274  2lgslem3  15342  2lgsoddprmlem3  15352  djulclALT  15447  djurclALT  15448  bj-charfun  15453  bj-nntrans  15597  bj-nnelirr  15599