Theorem elun 4155

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 3475	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3475	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3475	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 871	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2852	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2852	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 932	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 4154	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3637	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ∪ cun 4152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154

This theorem is used by:  elunnel1  4156  elunnel2  4157  uneqri  4158  uncom  4160  uneq1  4163  nfun  4172  unass  4173  ssun1  4179  elunant  4185  unss1  4186  ssequn1  4187  rexun  4197  elsymdif  4206  indi  4232  undi  4233  unineq  4236  undif3  4248  rabun2  4272  reuun2  4273  undif4  4423  ssundif  4446  dfpr2  4605  elunsn  4644  elpwunsn  4645  eltpg  4647  el7g  4651  pwpr  4831  pwtp  4832  uniun  4893  iinun2  5034  iunun  5056  iunxun  5057  iinuni  5061  brun  5159  trun  5226  pwssun  5547  opthprc  5719  xpundi  5724  xpundir  5725  difxp  6167  sossfld  6190  imadifssranOLD  6215  imadifssranOLDOLD  6216  elsuci  6450  elsucg  6451  elsuc2g  6452  funun  6606  mptun  6707  unima  6983  eqfnun  7059  unpreima  7086  ordsucun  7860  resf1extb  7970  fnse  8177  xpord2pred  8189  xpord3pred  8196  suppofssd  8248  reldmtpos  8279  dftpos4  8290  tpostpos  8291  frrlem12  8343  frrlem13  8344  oarec  8598  brdom2  9037  unfi  9214  unxpdomlem3  9277  domunfican  9341  dfsup2  9463  wemapso2lem  9573  unwdomg  9605  unxpwdom2  9609  cantnfp1lem3  9708  rankunb  9891  djur  10027  djuunxp  10029  eldju2ndl  10032  eldju2ndr  10033  djuun  10034  iscard3  10199  kmlem2  10257  ssfin4  10415  dffin7-2  10503  fin1a2lem11  10515  fin1a2lem12  10516  cfpwsdom  10696  elgch  10734  fpwwe2lem12  10754  canthp1lem2  10765  gch2  10787  elnn0  12635  un0addcl  12666  un0mulcl  12667  elxnn0  12708  ltxr  13271  elxr  13272  xrsupexmnf  13462  xrinfmexpnf  13463  supxrun  13473  ixxun  13519  difreicc  13642  iccsplit  13643  fzsplit2  13710  elfzp1  13735  uzsplit  13757  elfzp12  13764  fzosplit  13854  fzouzsplit  13856  elfzonlteqm1  13903  elfzo0l  13918  fzosplitsni  13941  elfzr  13943  elfzlmr  13944  hashnn0pnf  14513  hashf1lem2  14628  hash2pwpr  14648  pr2pwpr  14651  ccatrn  14762  cats1un  14898  fsumsplit  15936  sumsplit  15963  fprodsplit  16162  rpnnen2lem12  16422  sumeven  16586  sumodd  16587  saddisjlem  16663  lcmfunsnlem1  16841  lcmfunsnlem2lem1  16842  lcmfunsnlem2lem2  16843  lcmfunsnlem2  16844  coprmprod  16865  coprmproddvdslem  16866  nnnn0modprm0  17013  prm23lt5  17021  vdwapun  17181  ramubcl  17225  basprssdmsets  17428  mreexmrid  17846  lubun  18718  chnccats1  18828  smndex1basss  19133  smndex1mgm  19135  smndex1mndlem  19137  smndex1n0mnd  19140  symgextf1  19665  gsumzsplit  20171  gsumzunsnd  20200  gsumunsnfd  20201  dprddisj2  20285  dmdprdsplit2lem  20291  dmdprdsplit2  20292  dprdsplit  20294  cnfldfun  21722  mplcoe1  22376  mplcoe5  22379  evlslem4  22415  mdetunilem9  22965  maducoeval2  22985  madugsum  22988  clslp  23496  islpi  23497  restntr  23530  pnfnei  23568  mnfnei  23569  iunconn  23776  refun0  23864  xkoptsub  24003  ptunhmeo  24157  fbun  24189  filconn  24232  fixufil  24271  ufildr  24280  alexsubALTlem2  24397  alexsubALTlem3  24398  alexsubALTlem4  24399  tsmssplit  24501  xrtgioo  25156  reconnlem2  25177  iccpnfcnv  25295  iccpnfhmeo  25296  rrxcph  25743  rrxdstprj1  25760  mbfss  25997  mbfmax  26000  itg2splitlem  26099  itg2split  26100  iblss2  26156  itgsplit  26186  limcdif  26226  ellimc2  26227  limcmpt  26233  limcres  26236  limccnp  26241  limccnp2  26242  limcco  26243  rollelem  26339  dvivthlem1  26358  dvne0  26361  lhop  26366  degltlem1  26420  ply1rem  26514  fta1glem2  26517  plypf1  26561  plyaddlem1  26562  plymullem1  26563  plycj  26626  ofmulrt  26630  taylfval  26716  abelthlem2  26789  abelthlem3  26790  reasinsin  27254  scvxcvx  27343  ppinprm  27509  chtnprm  27511  dchrfi  27612  lgsdir2  27687  2lgslem3  27761  2lgsoddprmlem3  27771  nosepdmlem  28070  sltsun1  28204  sltsun2  28205  addsproplem2  28386  addsuniflem  28417  negsid  28457  mulsproplem9  28540  sltmuls1  28563  sltmuls2  28564  precsexlem9  28631  precsexlem11  28633  ltonold  28677  usgrexmplef  29870  cffldtocusgr  30058  vtxdun  30092  eucrct2eupth  30876  shunssi  32000  atomli  33014  atoml2i  33015  rmoun  33162  rmounid  33163  nelun  33181  suppovss  33345  isoun  33366  fzsplit3  33455  eliccioo  33567  gsumwun  33707  cycpmco2  33764  cyc3co2  33771  cycpmrn  33774  elrgspnlem2  33874  ply1dg3rt0irred  34186  lindsun  34327  lbsdiflsp0  34328  ordtconnlem1  34626  xrge0iifcnv  34635  xrge0iifiso  34637  xrge0iifhom  34639  esumsplit  34755  esumpad2  34758  measvuni  34917  sxbrsigalem0  34973  bnj1138  35489  bnj1137  35695  subfacp1lem4  36115  subfacp1lem5  36116  kur14lem7  36144  satfvsucsuc  36297  satfrnmapom  36302  satf0op  36309  satf0n0  36310  sat1el2xp  36311  fmlafvel  36317  isfmlasuc  36320  fmlaomn0  36322  satfv1fvfmla1  36355  2goelgoanfmla1  36356  mrsubcv  36442  mclsax  36501  brcup  36879  refssfne  37324  ttciunun  37477  bj-eltag  38068  bj-0eltag  38069  bj-sngltag  38074  bj-projun  38085  bj-axbun  38127  bj-axadj  38132  bj-imdirco  38303  tan2h  38727  poimirlem2  38732  poimirlem8  38738  poimirlem18  38748  poimirlem21  38751  poimirlem22  38752  poimirlem23  38753  poimirlem24  38754  poimirlem25  38755  poimirlem27  38757  poimirlem29  38759  poimirlem31  38761  poimirlem32  38762  ftc1anclem1  38803  ftc1anclem5  38807  dvasin  38814  dvacos  38815  smprngopr  39178  dfsucmap3  39587  elpadd  41048  paddval0  41059  hdmaplem4  43023  mapdh9a  43038  unitscyglem2  43438  ofun  43482  lzunuz  43972  jm2.23  44196  unxpwdom3  44290  hbtlem5  44322  fzunt  44648  fzuntd  44649  fzunt1d  44650  fzuntgd  44651  rp-fakeinunass  44708  sqrtcvallem1  44823  frege133d  44957  frege83  45138  frege131  45186  frege133  45188  uneqsn  45217  clsk1indlem3  45235  ntrneixb  45287  ntrneix3  45289  ntrneix13  45291  radcnvrat  45490  bccbc  45521  undif3VD  46055  iunconnlem2  46108  permaxinf2lem  46197  fnchoice  46251  limciccioolb  46838  limcicciooub  46852  icccncfext  47102  cncfiooicclem1  47108  fourierdlem70  47391  fourierdlem80  47401  fourierdlem93  47414  fourierdlem101  47422  sge0split  47624  wrddun2  48105  chndun2  48110  chnrun2  48115  el1fzopredsuc  48601  iccpartltu  48712  iccpartgtl  48713  iccpartgt  48714  iccpartleu  48715  iccpartgel  48716  fmtno4prmfac  48862  31prm  48887  sbgoldbo  49090  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  wtgoldbnnsum4prm  49105  bgoldbnnsum3prm  49107  bgoldbtbndlem3  49110  bgoldbtbnd  49112  elclnbgrelnbgr  49128  clnbgrel  49131  clnbupgrel  49137  dfclnbgr6  49159  isubgr3stgrlem4  49272  usgrexmpl1tri  49328  usgrexmpl2nb0  49334  usgrexmpl2nb1  49335  usgrexmpl2nb2  49336  usgrexmpl2nb3  49337  usgrexmpl2nb4  49338  usgrexmpl2nb5  49339  usgrexmpl2trifr  49340  gpgprismgr4cycllem3  49400  gpgprismgr4cycllem7  49404  gpgprismgr4cycllem10  49407  smprngprmrng  49641  parhomcl2  50950