Theorem elun 4113

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 3482	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3482	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3482	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 870	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2857	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2857	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 931	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3916	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3646	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 209   ∨ wo 860   = wceq 1567   ∈ wcel 2149  Vcvv 3461   ∪ cun 3909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-un 3916

This theorem is referenced by:  elunnel1  4114  elunnel2  4115  uneqri  4116  uncom  4118  uneq1  4121  nfun  4130  unass  4131  ssun1  4137  elunant  4143  unss1  4144  ssequn1  4145  rexun  4155  elsymdif  4217  indi  4243  undi  4244  unineq  4247  undif3  4259  rabun2  4283  reuun2  4284  undif4  4431  ssundif  4451  dfpr2  4613  elunsn  4652  elpwunsn  4653  eltpg  4655  el7g  4659  pwpr  4868  pwtp  4869  uniun  4897  iinun2  5039  iunun  5061  iunxun  5062  iinuni  5066  brun  5164  trun  5231  pwssun  5554  opthprc  5726  xpundi  5731  xpundir  5732  difxp  6162  sossfld  6185  imadifssran  6203  imadifssranOLD  6204  elsuci  6431  elsucg  6432  elsuc2g  6433  funun  6583  mptun  6682  unima  6957  eqfnun  7033  unpreima  7059  ordsucun  7821  resf1extb  7931  fnse  8129  xpord2pred  8141  xpord3pred  8148  suppofssd  8199  reldmtpos  8230  dftpos4  8241  tpostpos  8242  frrlem12  8294  frrlem13  8295  oarec  8547  brdom2  8979  unfi  9155  unxpdomlem3  9218  domunfican  9281  dfsup2  9404  wemapso2lem  9514  unwdomg  9546  unxpwdom2  9550  cantnfp1lem3  9649  rankunb  9822  djur  9905  djuunxp  9907  eldju2ndl  9910  eldju2ndr  9911  djuun  9912  iscard3  10077  kmlem2  10135  ssfin4  10294  dffin7-2  10382  fin1a2lem11  10394  fin1a2lem12  10395  cfpwsdom  10569  elgch  10607  fpwwe2lem12  10627  canthp1lem2  10638  gch2  10660  elnn0  12506  un0addcl  12537  un0mulcl  12538  elxnn0  12579  ltxr  13140  elxr  13141  xrsupexmnf  13331  xrinfmexpnf  13332  supxrun  13342  ixxun  13388  difreicc  13511  iccsplit  13512  fzsplit2  13577  elfzp1  13602  uzsplit  13624  elfzp12  13631  fzosplit  13721  fzouzsplit  13723  elfzonlteqm1  13770  elfzo0l  13785  fzosplitsni  13808  elfzr  13810  elfzlmr  13811  hashnn0pnf  14378  hashf1lem2  14493  hash2pwpr  14513  pr2pwpr  14516  ccatrn  14627  cats1un  14758  fsumsplit  15792  sumsplit  15819  fprodsplit  16020  rpnnen2lem12  16281  sumeven  16445  sumodd  16446  saddisjlem  16522  lcmfunsnlem1  16695  lcmfunsnlem2lem1  16696  lcmfunsnlem2lem2  16697  lcmfunsnlem2  16698  coprmprod  16719  coprmproddvdslem  16720  nnnn0modprm0  16866  prm23lt5  16874  vdwapun  17034  ramubcl  17078  basprssdmsets  17281  mreexmrid  17699  lubun  18571  chnccats1  18681  smndex1basss  18967  smndex1mgm  18969  smndex1mndlem  18971  smndex1n0mnd  18974  symgextf1  19491  gsumzsplit  19997  gsumzunsnd  20026  gsumunsnfd  20027  dprddisj2  20111  dmdprdsplit2lem  20117  dmdprdsplit2  20118  dprdsplit  20120  cnfldfun  21505  mplcoe1  22157  mplcoe5  22160  evlslem4  22196  mdetunilem9  22746  maducoeval2  22766  madugsum  22769  clslp  23274  islpi  23275  restntr  23308  pnfnei  23346  mnfnei  23347  iunconn  23554  refun0  23641  xkoptsub  23780  ptunhmeo  23934  fbun  23966  filconn  24009  fixufil  24048  ufildr  24057  alexsubALTlem2  24174  alexsubALTlem3  24175  alexsubALTlem4  24176  tsmssplit  24278  xrtgioo  24933  reconnlem2  24954  iccpnfcnv  25072  iccpnfhmeo  25073  rrxcph  25520  rrxdstprj1  25537  mbfss  25774  mbfmax  25777  itg2splitlem  25876  itg2split  25877  iblss2  25934  itgsplit  25964  limcdif  26004  ellimc2  26005  limcmpt  26011  limcres  26014  limccnp  26019  limccnp2  26020  limcco  26021  rollelem  26117  dvivthlem1  26136  dvne0  26139  lhop  26144  degltlem1  26198  ply1rem  26292  fta1glem2  26295  plypf1  26338  plyaddlem1  26339  plymullem1  26340  plycj  26403  plycjOLD  26405  ofmulrt  26409  taylfval  26488  abelthlem2  26561  abelthlem3  26562  reasinsin  27027  scvxcvx  27116  ppinprm  27282  chtnprm  27284  dchrfi  27385  lgsdir2  27460  2lgslem3  27534  2lgsoddprmlem3  27544  nosepdmlem  27813  sltsun1  27947  sltsun2  27948  addsproplem2  28129  addsuniflem  28160  negsid  28200  mulsproplem9  28283  sltmuls1  28306  sltmuls2  28307  precsexlem9  28374  precsexlem11  28376  ltonold  28420  usgrexmplef  29550  cffldtocusgr  29738  vtxdun  29772  eucrct2eupth  30537  shunssi  31661  atomli  32675  atoml2i  32676  rmoun  32781  rmounid  32782  nelun  32800  suppovss  32967  isoun  32988  fzsplit3  33079  eliccioo  33191  gsumwun  33337  cycpmco2  33394  cyc3co2  33401  cycpmrn  33404  elrgspnlem2  33504  ply1dg3rt0irred  33819  lindsun  33960  lbsdiflsp0  33961  ordtconnlem1  34259  xrge0iifcnv  34268  xrge0iifiso  34270  xrge0iifhom  34272  esumsplit  34388  esumpad2  34391  measvuni  34549  sxbrsigalem0  34606  bnj1138  35122  bnj1137  35328  subfacp1lem4  35608  subfacp1lem5  35609  kur14lem7  35637  satfvsucsuc  35790  satfrnmapom  35795  satf0op  35802  satf0n0  35803  sat1el2xp  35804  fmlafvel  35810  isfmlasuc  35813  fmlaomn0  35815  satfv1fvfmla1  35848  2goelgoanfmla1  35849  mrsubcv  35935  mclsax  35994  brcup  36362  refssfne  36792  ttciunun  36945  bj-eltag  37536  bj-0eltag  37537  bj-sngltag  37542  bj-projun  37553  bj-axbun  37595  bj-axadj  37600  bj-imdirco  37757  tan2h  38186  poimirlem2  38196  poimirlem8  38202  poimirlem18  38212  poimirlem21  38215  poimirlem22  38216  poimirlem23  38217  poimirlem24  38218  poimirlem25  38219  poimirlem27  38221  poimirlem29  38223  poimirlem31  38225  poimirlem32  38226  ftc1anclem1  38267  ftc1anclem5  38271  dvasin  38278  dvacos  38279  smprngopr  38626  dfsucmap3  39037  elpadd  40498  paddval0  40509  hdmaplem4  42473  mapdh9a  42488  unitscyglem2  42888  ofun  42931  lzunuz  43426  jm2.23  43650  unxpwdom3  43749  hbtlem5  43782  fzunt  44108  fzuntd  44109  fzunt1d  44110  fzuntgd  44111  rp-fakeinunass  44168  sqrtcvallem1  44284  frege133d  44418  frege83  44599  frege131  44647  frege133  44649  uneqsn  44678  clsk1indlem3  44696  ntrneixb  44748  ntrneix3  44750  ntrneix13  44752  radcnvrat  44951  bccbc  44982  undif3VD  45517  iunconnlem2  45570  permaxinf2lem  45648  fnchoice  45676  limciccioolb  46264  limcicciooub  46278  icccncfext  46528  cncfiooicclem1  46534  fourierdlem70  46817  fourierdlem80  46827  fourierdlem93  46840  fourierdlem101  46848  sge0split  47050  el1fzopredsuc  47987  iccpartltu  48098  iccpartgtl  48099  iccpartgt  48100  iccpartleu  48101  iccpartgel  48102  fmtno4prmfac  48248  31prm  48273  sbgoldbo  48476  nnsum4primeseven  48489  nnsum4primesevenALTV  48490  wtgoldbnnsum4prm  48491  bgoldbnnsum3prm  48493  bgoldbtbndlem3  48496  bgoldbtbnd  48498  elclnbgrelnbgr  48514  clnbgrel  48517  clnbupgrel  48523  dfclnbgr6  48545  isubgr3stgrlem4  48658  usgrexmpl1tri  48714  usgrexmpl2nb0  48720  usgrexmpl2nb1  48721  usgrexmpl2nb2  48722  usgrexmpl2nb3  48723  usgrexmpl2nb4  48724  usgrexmpl2nb5  48725  usgrexmpl2trifr  48726  gpgprismgr4cycllem3  48786  gpgprismgr4cycllem7  48790  gpgprismgr4cycllem10  48793  smprngprmrng  49028