Theorem elun 3348

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

Syntax hints:   ↔ wb 105   ∨ wo 715   = wceq 1397   ∈ wcel 2202  Vcvv 2802   ∪ cun 3198

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204

This theorem is referenced by:  uneqri  3349  uncom  3351  uneq1  3354  unass  3364  ssun1  3370  unss1  3376  ssequn1  3377  unss  3381  rexun  3387  ralunb  3388  unssdif  3442  unssin  3446  inssun  3447  indi  3454  undi  3455  difundi  3459  difindiss  3461  undif3ss  3468  symdifxor  3473  rabun2  3486  reuun2  3490  undif4  3557  ssundifim  3578  dcun  3604  dfpr2  3688  eltpg  3714  pwprss  3889  pwtpss  3890  uniun  3912  intun  3959  iunun  4049  iunxun  4050  iinuniss  4053  brun  4140  undifexmid  4283  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  pwunss  4380  elsuci  4500  elsucg  4501  elsuc2g  4502  ordsucim  4598  sucprcreg  4647  opthprc  4777  xpundi  4782  xpundir  4783  funun  5371  mptun  5464  unpreima  5772  reldmtpos  6419  dftpos4  6429  tpostpos  6430  elssdc  7094  onunsnss  7109  unfidisj  7114  undifdcss  7115  fidcenumlemrks  7152  djulclb  7254  eldju  7267  eldju2ndl  7271  eldju2ndr  7272  ctssdccl  7310  pw1nel3  7449  sucpw1nel3  7451  elnn0  9404  un0addcl  9435  un0mulcl  9436  elxnn0  9467  ltxr  10010  elxr  10011  fzsplit2  10285  elfzp1  10307  uzsplit  10327  elfzp12  10334  fz01or  10346  fzosplit  10414  fzouzsplit  10416  elfzonlteqm1  10456  fzosplitsni  10482  hashinfuni  11040  hashennnuni  11042  hashunlem  11068  zfz1isolemiso  11104  ccatrn  11187  cats1un  11303  summodclem3  11943  fsumsplit  11970  fsumsplitsn  11973  sumsplitdc  11995  fprodsplitdc  12159  fprodsplit  12160  fprodunsn  12167  fprodsplitsn  12196  nnnn0modprm0  12830  prm23lt5  12838  reopnap  15273  plyaddlem1  15474  plymullem1  15475  plycoeid3  15484  plycj  15488  lgsdir2  15765  2lgslem3  15833  2lgsoddprmlem3  15843  vtxdfifiun  16151  djulclALT  16418  djurclALT  16419  bj-charfun  16423  bj-nntrans  16567  bj-nnelirr  16569