Theorem elun 3905

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 3364	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3364	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3364	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 838	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2838	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2838	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 896	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3729	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3505	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 367	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 196   ∨ wo 828   = wceq 1631   ∈ wcel 2145  Vcvv 3351   ∪ cun 3722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3729

This theorem is referenced by:  elunnel1  3906  uneqri  3907  uncom  3909  uneq1  3912  unass  3922  ssun1  3928  unss1  3934  ssequn1  3935  unss  3939  rexun  3945  ralunb  3946  elsymdif  3999  symdif2  4002  indi  4023  undi  4024  unineq  4027  undif3  4038  rabun2  4055  reuun2  4059  undif4  4178  ssundif  4195  dfpr2  4335  elpwunsn  4363  eltpg  4365  pwpr  4569  pwtp  4570  uniun  4594  intun  4644  iinun2  4721  iunun  4739  iunxun  4740  iinuni  4744  brun  4838  pwunss  5153  pwssun  5154  opthprc  5308  xpundi  5312  xpundir  5313  difxp  5700  sossfld  5722  elsuci  5935  elsucg  5936  elsuc2g  5937  funun  6076  mptun  6166  unpreima  6485  suceloni  7161  ordsucun  7173  fnse  7446  reldmtpos  7513  dftpos4  7524  tpostpos  7525  wfrlem14  7582  wfrlem15  7583  oarec  7797  brdom2  8140  unxpdomlem3  8323  domunfican  8390  dfsup2  8507  wemapso2lem  8614  unwdomg  8646  unxpwdom2  8650  cantnfp1lem3  8742  rankunb  8878  djur  8946  djuunxp  8948  eldju2ndl  8951  eldju2ndr  8952  djuun  8953  iscard3  9117  kmlem2  9176  ssfin4  9335  dffin7-2  9423  fin1a2lem11  9435  fin1a2lem12  9436  cfpwsdom  9609  elgch  9647  fpwwe2lem13  9667  canthp1lem2  9678  gch2  9700  elnn0  11497  un0addcl  11529  un0mulcl  11530  elxnn0  11568  ltxr  12155  elxr  12156  xrsupexmnf  12341  xrinfmexpnf  12342  supxrun  12352  ixxun  12397  difreicc  12512  iccsplit  12513  fzsplit2  12574  elfzp1  12599  uzsplit  12620  elfzp12  12627  fzosplit  12710  fzouzsplit  12712  elfzonlteqm1  12753  elfzo0l  12767  fzosplitsni  12788  elfzr  12790  elfzlmr  12791  hashnn0pnf  13335  hashf1lem2  13443  hash2pwpr  13461  pr2pwpr  13464  ccatrn  13572  cats1un  13685  fsumsplit  14680  sumsplit  14708  fprodsplit  14904  rpnnen2lem12  15161  sumeven  15319  sumodd  15320  saddisjlem  15395  lcmfunsnlem1  15559  lcmfunsnlem2lem1  15560  lcmfunsnlem2lem2  15561  lcmfunsnlem2  15562  coprmprod  15583  coprmproddvdslem  15584  nnnn0modprm0  15719  prm23lt5  15727  vdwapun  15886  ramubcl  15930  basprssdmsets  16133  xpsfrnel2  16434  mreexmrid  16512  lubun  17332  symgextf1  18049  gsumzsplit  18535  gsumzunsnd  18563  gsumunsnfd  18564  dprddisj2  18647  dmdprdsplit2lem  18653  dmdprdsplit2  18654  dprdsplit  18656  mplcoe1  19681  mplcoe5  19684  evlslem4  19724  cnfldfunALT  19975  mdetunilem9  20645  maducoeval2  20665  madugsum  20668  clslp  21174  islpi  21175  restntr  21208  pnfnei  21246  mnfnei  21247  iunconn  21453  refun0  21540  xkoptsub  21679  ptunhmeo  21833  fbun  21865  filconn  21908  fixufil  21947  ufildr  21956  alexsubALTlem2  22073  alexsubALTlem3  22074  alexsubALTlem4  22075  tsmssplit  22176  xrtgioo  22830  reconnlem2  22851  iccpnfcnv  22964  iccpnfhmeo  22965  rrxcph  23400  rrxdstprj1  23412  mbfss  23634  mbfmax  23637  itg2splitlem  23736  itg2split  23737  iblss2  23793  itgsplit  23823  limcdif  23861  ellimc2  23862  limcmpt  23868  limcres  23871  limccnp  23876  limccnp2  23877  limcco  23878  rollelem  23973  dvivthlem1  23992  dvne0  23995  lhop  24000  degltlem1  24053  ply1rem  24144  fta1glem2  24147  plypf1  24189  plyaddlem1  24190  plymullem1  24191  plycj  24254  ofmulrt  24258  taylfval  24334  abelthlem2  24407  abelthlem3  24408  reasinsin  24845  scvxcvx  24934  ppinprm  25100  chtnprm  25102  dchrfi  25202  lgsdir2  25277  2lgslem3  25351  2lgsoddprmlem3  25361  usgrexmplef  26375  cffldtocusgr  26579  vtxdun  26613  eucrct2eupth  27426  shunssi  28568  atomli  29582  atoml2i  29583  isoun  29820  fzsplit3  29894  eliccioo  29980  ordtconnlem1  30311  xrge0iifcnv  30320  xrge0iifiso  30322  xrge0iifhom  30324  esumsplit  30456  esumpad2  30459  measvuni  30618  sxbrsigalem0  30674  bnj1138  31198  bnj1137  31402  subfacp1lem4  31504  subfacp1lem5  31505  kur14lem7  31533  mrsubcv  31746  mclsax  31805  dftrpred3g  32070  nosepdmlem  32171  brcup  32384  refssfne  32691  bj-eltag  33297  bj-0eltag  33298  bj-sngltag  33303  bj-projun  33314  tan2h  33735  poimirlem2  33745  poimirlem8  33751  poimirlem18  33761  poimirlem21  33764  poimirlem22  33765  poimirlem23  33766  poimirlem24  33767  poimirlem25  33768  poimirlem27  33770  poimirlem29  33772  poimirlem31  33774  poimirlem32  33775  ftc1anclem1  33818  ftc1anclem5  33822  dvasin  33829  dvacos  33830  eqfnun  33849  smprngopr  34184  elpadd  35608  paddval0  35619  hdmaplem4  37585  mapdh9a  37600  lzunuz  37858  jm2.23  38090  unxpwdom3  38192  hbtlem5  38225  rp-fakeinunass  38388  frege133d  38584  frege83  38767  frege131  38815  frege133  38817  uneqsn  38848  clsk1indlem3  38868  ntrneixb  38920  ntrneix3  38922  ntrneix13  38924  radcnvrat  39040  bccbc  39071  undif3VD  39641  iunconnlem2  39694  fnchoice  39711  elunnel2  39721  unima  39867  limciccioolb  40372  limcicciooub  40388  icccncfext  40619  cncfiooicclem1  40625  fourierdlem70  40911  fourierdlem80  40921  fourierdlem93  40934  fourierdlem101  40942  sge0split  41144  el1fzopredsuc  41864  iccpartltu  41890  iccpartgtl  41891  iccpartgt  41892  iccpartleu  41893  iccpartgel  41894  fmtno4prmfac  42013  31prm  42041  sbgoldbo  42204  nnsum4primeseven  42217  nnsum4primesevenALTV  42218  wtgoldbnnsum4prm  42219  bgoldbnnsum3prm  42221  bgoldbtbndlem3  42224  bgoldbtbnd  42226