Theorem elun 3277

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 2749	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 2749	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 2749	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 716	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2240	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2240	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 793	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3134	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2885	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 704	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 105   ∨ wo 708   = wceq 1353   ∈ wcel 2148  Vcvv 2738   ∪ cun 3128

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134

This theorem is referenced by:  uneqri  3278  uncom  3280  uneq1  3283  unass  3293  ssun1  3299  unss1  3305  ssequn1  3306  unss  3310  rexun  3316  ralunb  3317  unssdif  3371  unssin  3375  inssun  3376  indi  3383  undi  3384  difundi  3388  difindiss  3390  undif3ss  3397  symdifxor  3402  rabun2  3415  reuun2  3419  undif4  3486  ssundifim  3507  dcun  3534  dfpr2  3612  eltpg  3638  pwprss  3806  pwtpss  3807  uniun  3829  intun  3876  iunun  3966  iunxun  3967  iinuniss  3970  brun  4055  undifexmid  4194  exmidundif  4207  exmidundifim  4208  exmid1stab  4209  pwunss  4284  elsuci  4404  elsucg  4405  elsuc2g  4406  ordsucim  4500  sucprcreg  4549  opthprc  4678  xpundi  4683  xpundir  4684  funun  5261  mptun  5348  unpreima  5642  reldmtpos  6254  dftpos4  6264  tpostpos  6265  onunsnss  6916  unfidisj  6921  undifdcss  6922  fidcenumlemrks  6952  djulclb  7054  eldju  7067  eldju2ndl  7071  eldju2ndr  7072  ctssdccl  7110  pw1nel3  7230  sucpw1nel3  7232  elnn0  9178  un0addcl  9209  un0mulcl  9210  elxnn0  9241  ltxr  9775  elxr  9776  fzsplit2  10050  elfzp1  10072  uzsplit  10092  elfzp12  10099  fz01or  10111  fzosplit  10177  fzouzsplit  10179  elfzonlteqm1  10210  fzosplitsni  10235  hashinfuni  10757  hashennnuni  10759  hashunlem  10784  zfz1isolemiso  10819  summodclem3  11388  fsumsplit  11415  fsumsplitsn  11418  sumsplitdc  11440  fprodsplitdc  11604  fprodsplit  11605  fprodunsn  11612  fprodsplitsn  11641  nnnn0modprm0  12255  prm23lt5  12263  reopnap  14041  lgsdir2  14437  2lgsoddprmlem3  14462  djulclALT  14556  djurclALT  14557  bj-charfun  14562  bj-nntrans  14706  bj-nnelirr  14708