Theorem elun 4116

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 3468	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3468	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3468	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 857	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2816	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2816	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 918	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3919	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3647	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1540   ∈ wcel 2109  Vcvv 3447   ∪ cun 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919

This theorem is referenced by:  elunnel1  4117  elunnel2  4118  uneqri  4119  uncom  4121  uneq1  4124  nfun  4133  unass  4135  ssun1  4141  elunant  4147  unss1  4148  ssequn1  4149  rexun  4159  elsymdif  4221  indi  4247  undi  4248  unineq  4251  undif3  4263  rabun2  4287  reuun2  4288  undif4  4430  ssundif  4451  dfpr2  4610  elunsn  4647  elpwunsn  4648  eltpg  4650  el7g  4654  pwpr  4865  pwtp  4866  uniun  4894  iinun2  5037  iunun  5057  iunxun  5058  iinuni  5062  brun  5158  pwssun  5530  opthprc  5702  xpundi  5707  xpundir  5708  imadifssran  6124  difxp  6137  sossfld  6159  elsuci  6401  elsucg  6402  elsuc2g  6403  funun  6562  mptun  6664  unima  6936  eqfnun  7009  unpreima  7035  sucexeloniOLD  7786  ordsucun  7800  resf1extb  7910  fnse  8112  xpord2pred  8124  xpord3pred  8131  suppofssd  8182  reldmtpos  8213  dftpos4  8224  tpostpos  8225  frrlem12  8276  frrlem13  8277  oarec  8526  brdom2  8953  unfi  9135  unxpdomlem3  9199  domunfican  9272  dfsup2  9395  wemapso2lem  9505  unwdomg  9537  unxpwdom2  9541  cantnfp1lem3  9633  rankunb  9803  djur  9872  djuunxp  9874  eldju2ndl  9877  eldju2ndr  9878  djuun  9879  iscard3  10046  kmlem2  10105  ssfin4  10263  dffin7-2  10351  fin1a2lem11  10363  fin1a2lem12  10364  cfpwsdom  10537  elgch  10575  fpwwe2lem12  10595  canthp1lem2  10606  gch2  10628  elnn0  12444  un0addcl  12475  un0mulcl  12476  elxnn0  12517  ltxr  13075  elxr  13076  xrsupexmnf  13265  xrinfmexpnf  13266  supxrun  13276  ixxun  13322  difreicc  13445  iccsplit  13446  fzsplit2  13510  elfzp1  13535  uzsplit  13557  elfzp12  13564  fzosplit  13653  fzouzsplit  13655  elfzonlteqm1  13702  elfzo0l  13717  fzosplitsni  13739  elfzr  13741  elfzlmr  13742  hashnn0pnf  14307  hashf1lem2  14421  hash2pwpr  14441  pr2pwpr  14444  ccatrn  14554  cats1un  14686  fsumsplit  15707  sumsplit  15734  fprodsplit  15932  rpnnen2lem12  16193  sumeven  16357  sumodd  16358  saddisjlem  16434  lcmfunsnlem1  16607  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  lcmfunsnlem2  16610  coprmprod  16631  coprmproddvdslem  16632  nnnn0modprm0  16777  prm23lt5  16785  vdwapun  16945  ramubcl  16989  basprssdmsets  17191  mreexmrid  17604  lubun  18474  smndex1basss  18832  smndex1mgm  18834  smndex1mndlem  18836  smndex1n0mnd  18839  symgextf1  19351  gsumzsplit  19857  gsumzunsnd  19886  gsumunsnfd  19887  dprddisj2  19971  dmdprdsplit2lem  19977  dmdprdsplit2  19978  dprdsplit  19980  cnfldfun  21278  cnfldfunOLD  21291  mplcoe1  21944  mplcoe5  21947  evlslem4  21983  mdetunilem9  22507  maducoeval2  22527  madugsum  22530  clslp  23035  islpi  23036  restntr  23069  pnfnei  23107  mnfnei  23108  iunconn  23315  refun0  23402  xkoptsub  23541  ptunhmeo  23695  fbun  23727  filconn  23770  fixufil  23809  ufildr  23818  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  tsmssplit  24039  xrtgioo  24695  reconnlem2  24716  iccpnfcnv  24842  iccpnfhmeo  24843  rrxcph  25292  rrxdstprj1  25309  mbfss  25547  mbfmax  25550  itg2splitlem  25649  itg2split  25650  iblss2  25707  itgsplit  25737  limcdif  25777  ellimc2  25778  limcmpt  25784  limcres  25787  limccnp  25792  limccnp2  25793  limcco  25794  rollelem  25893  dvivthlem1  25913  dvne0  25916  lhop  25921  degltlem1  25977  ply1rem  26071  fta1glem2  26074  plypf1  26117  plyaddlem1  26118  plymullem1  26119  plycj  26183  plycjOLD  26185  ofmulrt  26189  taylfval  26266  abelthlem2  26342  abelthlem3  26343  reasinsin  26806  scvxcvx  26896  ppinprm  27062  chtnprm  27064  dchrfi  27166  lgsdir2  27241  2lgslem3  27315  2lgsoddprmlem3  27325  nosepdmlem  27595  ssltun1  27720  ssltun2  27721  addsproplem2  27877  addsuniflem  27908  negsid  27947  mulsproplem9  28027  ssltmul1  28050  ssltmul2  28051  precsexlem9  28117  precsexlem11  28119  sltonold  28162  usgrexmplef  29186  cffldtocusgr  29374  cffldtocusgrOLD  29375  vtxdun  29409  eucrct2eupth  30174  shunssi  31297  atomli  32311  atoml2i  32312  rmoun  32423  rmounid  32424  nelun  32442  suppovss  32604  isoun  32625  fzsplit3  32716  eliccioo  32851  chnccats1  32941  gsumwun  33005  cycpmco2  33090  cyc3co2  33097  cycpmrn  33100  elrgspnlem2  33194  ply1dg3rt0irred  33551  lindsun  33621  lbsdiflsp0  33622  ordtconnlem1  33914  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  esumsplit  34043  esumpad2  34046  measvuni  34204  sxbrsigalem0  34262  bnj1138  34778  bnj1137  34985  subfacp1lem4  35170  subfacp1lem5  35171  kur14lem7  35199  satfvsucsuc  35352  satfrnmapom  35357  satf0op  35364  satf0n0  35365  sat1el2xp  35366  fmlafvel  35372  isfmlasuc  35375  fmlaomn0  35377  satfv1fvfmla1  35410  2goelgoanfmla1  35411  mrsubcv  35497  mclsax  35556  brcup  35927  refssfne  36346  bj-eltag  36965  bj-0eltag  36966  bj-sngltag  36971  bj-projun  36982  bj-axbun  37024  bj-axadj  37029  bj-imdirco  37178  tan2h  37606  poimirlem2  37616  poimirlem8  37622  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem27  37641  poimirlem29  37643  poimirlem31  37645  poimirlem32  37646  ftc1anclem1  37687  ftc1anclem5  37691  dvasin  37698  dvacos  37699  smprngopr  38046  elpadd  39793  paddval0  39804  hdmaplem4  41768  mapdh9a  41783  unitscyglem2  42184  ofun  42224  lzunuz  42756  jm2.23  42985  unxpwdom3  43084  hbtlem5  43117  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  rp-fakeinunass  43504  sqrtcvallem1  43620  frege133d  43754  frege83  43935  frege131  43983  frege133  43985  uneqsn  44014  clsk1indlem3  44032  ntrneixb  44084  ntrneix3  44086  ntrneix13  44088  radcnvrat  44303  bccbc  44334  undif3VD  44871  iunconnlem2  44924  permaxinf2lem  45002  fnchoice  45023  limciccioolb  45619  limcicciooub  45635  icccncfext  45885  cncfiooicclem1  45891  fourierdlem70  46174  fourierdlem80  46184  fourierdlem93  46197  fourierdlem101  46205  sge0split  46407  el1fzopredsuc  47326  iccpartltu  47426  iccpartgtl  47427  iccpartgt  47428  iccpartleu  47429  iccpartgel  47430  fmtno4prmfac  47573  31prm  47598  sbgoldbo  47788  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  bgoldbtbndlem3  47808  bgoldbtbnd  47810  elclnbgrelnbgr  47826  clnbgrel  47829  clnbupgrel  47835  dfclnbgr6  47856  isubgr3stgrlem4  47968  usgrexmpl1tri  48016  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  usgrexmpl2trifr  48028  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem7  48091  gpgprismgr4cycllem10  48094