Theorem elun 3347

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 2813	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2813	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2813	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 723	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2293	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2293	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 800	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3203	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2952	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 711	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 105   ∨ wo 715   = wceq 1397   ∈ wcel 2201  Vcvv 2801   ∪ cun 3197

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-un 3203

This theorem is referenced by:  uneqri  3348  uncom  3350  uneq1  3353  unass  3363  ssun1  3369  unss1  3375  ssequn1  3376  unss  3380  rexun  3386  ralunb  3387  unssdif  3441  unssin  3445  inssun  3446  indi  3453  undi  3454  difundi  3458  difindiss  3460  undif3ss  3467  symdifxor  3472  rabun2  3485  reuun2  3489  undif4  3556  ssundifim  3577  dcun  3603  dfpr2  3689  eltpg  3715  pwprss  3890  pwtpss  3891  uniun  3913  intun  3960  iunun  4050  iunxun  4051  iinuniss  4054  brun  4141  undifexmid  4285  exmidundif  4298  exmidundifim  4299  exmid1stab  4300  pwunss  4382  elsuci  4502  elsucg  4503  elsuc2g  4504  ordsucim  4600  sucprcreg  4649  opthprc  4779  xpundi  4784  xpundir  4785  funun  5373  mptun  5466  unpreima  5775  reldmtpos  6424  dftpos4  6434  tpostpos  6435  elssdc  7099  onunsnss  7114  unfidisj  7119  undifdcss  7120  fidcenumlemrks  7157  djulclb  7259  eldju  7272  eldju2ndl  7276  eldju2ndr  7277  ctssdccl  7315  pw1nel3  7454  sucpw1nel3  7456  elnn0  9409  un0addcl  9440  un0mulcl  9441  elxnn0  9472  ltxr  10015  elxr  10016  fzsplit2  10290  elfzp1  10312  uzsplit  10332  elfzp12  10339  fz01or  10351  fzosplit  10419  fzouzsplit  10421  elfzonlteqm1  10461  fzosplitsni  10487  hashinfuni  11045  hashennnuni  11047  hashunlem  11073  zfz1isolemiso  11109  ccatrn  11195  cats1un  11311  summodclem3  11964  fsumsplit  11991  fsumsplitsn  11994  sumsplitdc  12016  fprodsplitdc  12180  fprodsplit  12181  fprodunsn  12188  fprodsplitsn  12217  nnnn0modprm0  12851  prm23lt5  12859  reopnap  15299  plyaddlem1  15500  plymullem1  15501  plycoeid3  15510  plycj  15514  lgsdir2  15791  2lgslem3  15859  2lgsoddprmlem3  15869  vtxdfifiun  16177  djulclALT  16458  djurclALT  16459  bj-charfun  16462  bj-nntrans  16606  bj-nnelirr  16608