Theorem elun 3325

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 2791	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2791	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2791	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 720	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2272	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2272	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 797	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3181	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2930	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 708	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 105   ∨ wo 712   = wceq 1375   ∈ wcel 2180  Vcvv 2779   ∪ cun 3175

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-v 2781  df-un 3181

This theorem is referenced by:  uneqri  3326  uncom  3328  uneq1  3331  unass  3341  ssun1  3347  unss1  3353  ssequn1  3354  unss  3358  rexun  3364  ralunb  3365  unssdif  3419  unssin  3423  inssun  3424  indi  3431  undi  3432  difundi  3436  difindiss  3438  undif3ss  3445  symdifxor  3450  rabun2  3463  reuun2  3467  undif4  3534  ssundifim  3555  dcun  3581  dfpr2  3665  eltpg  3691  pwprss  3863  pwtpss  3864  uniun  3886  intun  3933  iunun  4023  iunxun  4024  iinuniss  4027  brun  4114  undifexmid  4256  exmidundif  4269  exmidundifim  4270  exmid1stab  4271  pwunss  4351  elsuci  4471  elsucg  4472  elsuc2g  4473  ordsucim  4569  sucprcreg  4618  opthprc  4747  xpundi  4752  xpundir  4753  funun  5338  mptun  5431  unpreima  5733  reldmtpos  6369  dftpos4  6379  tpostpos  6380  onunsnss  7047  unfidisj  7052  undifdcss  7053  fidcenumlemrks  7088  djulclb  7190  eldju  7203  eldju2ndl  7207  eldju2ndr  7208  ctssdccl  7246  pw1nel3  7384  sucpw1nel3  7386  elnn0  9339  un0addcl  9370  un0mulcl  9371  elxnn0  9402  ltxr  9939  elxr  9940  fzsplit2  10214  elfzp1  10236  uzsplit  10256  elfzp12  10263  fz01or  10275  fzosplit  10343  fzouzsplit  10345  elfzonlteqm1  10383  fzosplitsni  10408  hashinfuni  10966  hashennnuni  10968  hashunlem  10993  zfz1isolemiso  11028  ccatrn  11110  cats1un  11219  summodclem3  11857  fsumsplit  11884  fsumsplitsn  11887  sumsplitdc  11909  fprodsplitdc  12073  fprodsplit  12074  fprodunsn  12081  fprodsplitsn  12110  nnnn0modprm0  12744  prm23lt5  12752  reopnap  15185  plyaddlem1  15386  plymullem1  15387  plycoeid3  15396  plycj  15400  lgsdir2  15677  2lgslem3  15745  2lgsoddprmlem3  15755  djulclALT  16075  djurclALT  16076  bj-charfun  16080  bj-nntrans  16224  bj-nnelirr  16226