Theorem elun 3300

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

Syntax hints:   ↔ wb 105   ∨ wo 709   = wceq 1364   ∈ wcel 2164  Vcvv 2760   ∪ cun 3151

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157

This theorem is referenced by:  uneqri  3301  uncom  3303  uneq1  3306  unass  3316  ssun1  3322  unss1  3328  ssequn1  3329  unss  3333  rexun  3339  ralunb  3340  unssdif  3394  unssin  3398  inssun  3399  indi  3406  undi  3407  difundi  3411  difindiss  3413  undif3ss  3420  symdifxor  3425  rabun2  3438  reuun2  3442  undif4  3509  ssundifim  3530  dcun  3556  dfpr2  3637  eltpg  3663  pwprss  3831  pwtpss  3832  uniun  3854  intun  3901  iunun  3991  iunxun  3992  iinuniss  3995  brun  4080  undifexmid  4222  exmidundif  4235  exmidundifim  4236  exmid1stab  4237  pwunss  4314  elsuci  4434  elsucg  4435  elsuc2g  4436  ordsucim  4532  sucprcreg  4581  opthprc  4710  xpundi  4715  xpundir  4716  funun  5298  mptun  5385  unpreima  5683  reldmtpos  6306  dftpos4  6316  tpostpos  6317  onunsnss  6973  unfidisj  6978  undifdcss  6979  fidcenumlemrks  7012  djulclb  7114  eldju  7127  eldju2ndl  7131  eldju2ndr  7132  ctssdccl  7170  pw1nel3  7291  sucpw1nel3  7293  elnn0  9242  un0addcl  9273  un0mulcl  9274  elxnn0  9305  ltxr  9841  elxr  9842  fzsplit2  10116  elfzp1  10138  uzsplit  10158  elfzp12  10165  fz01or  10177  fzosplit  10244  fzouzsplit  10246  elfzonlteqm1  10277  fzosplitsni  10302  hashinfuni  10848  hashennnuni  10850  hashunlem  10875  zfz1isolemiso  10910  summodclem3  11523  fsumsplit  11550  fsumsplitsn  11553  sumsplitdc  11575  fprodsplitdc  11739  fprodsplit  11740  fprodunsn  11747  fprodsplitsn  11776  nnnn0modprm0  12393  prm23lt5  12401  reopnap  14706  plyaddlem1  14893  plymullem1  14894  lgsdir2  15149  2lgsoddprmlem3  15199  djulclALT  15293  djurclALT  15294  bj-charfun  15299  bj-nntrans  15443  bj-nnelirr  15445