Theorem elun 4133

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936

This theorem is referenced by:  elunnel1  4134  elunnel2  4135  uneqri  4136  uncom  4138  uneq1  4141  nfun  4150  unass  4152  ssun1  4158  elunant  4164  unss1  4165  ssequn1  4166  rexun  4176  elsymdif  4238  indi  4264  undi  4265  unineq  4268  undif3  4280  rabun2  4304  reuun2  4305  undif4  4447  ssundif  4468  dfpr2  4627  elunsn  4664  elpwunsn  4665  eltpg  4667  el7g  4671  pwpr  4882  pwtp  4883  uniun  4911  iinun2  5054  iunun  5074  iunxun  5075  iinuni  5079  brun  5175  pwssun  5550  opthprc  5723  xpundi  5728  xpundir  5729  imadifssran  6145  difxp  6158  sossfld  6180  elsuci  6426  elsucg  6427  elsuc2g  6428  funun  6587  mptun  6689  unima  6959  eqfnun  7032  unpreima  7058  sucexeloniOLD  7809  suceloniOLD  7811  ordsucun  7824  resf1extb  7935  fnse  8137  xpord2pred  8149  xpord3pred  8156  suppofssd  8207  reldmtpos  8238  dftpos4  8249  tpostpos  8250  frrlem12  8301  frrlem13  8302  wfrlem14OLD  8341  wfrlem15OLD  8342  oarec  8579  brdom2  9001  unfi  9190  unxpdomlem3  9265  domunfican  9338  dfsup2  9461  wemapso2lem  9571  unwdomg  9603  unxpwdom2  9607  cantnfp1lem3  9699  rankunb  9869  djur  9938  djuunxp  9940  eldju2ndl  9943  eldju2ndr  9944  djuun  9945  iscard3  10112  kmlem2  10171  ssfin4  10329  dffin7-2  10417  fin1a2lem11  10429  fin1a2lem12  10430  cfpwsdom  10603  elgch  10641  fpwwe2lem12  10661  canthp1lem2  10672  gch2  10694  elnn0  12508  un0addcl  12539  un0mulcl  12540  elxnn0  12581  ltxr  13136  elxr  13137  xrsupexmnf  13326  xrinfmexpnf  13327  supxrun  13337  ixxun  13383  difreicc  13506  iccsplit  13507  fzsplit2  13571  elfzp1  13596  uzsplit  13618  elfzp12  13625  fzosplit  13714  fzouzsplit  13716  elfzonlteqm1  13762  elfzo0l  13777  fzosplitsni  13799  elfzr  13801  elfzlmr  13802  hashnn0pnf  14365  hashf1lem2  14479  hash2pwpr  14499  pr2pwpr  14502  ccatrn  14612  cats1un  14744  fsumsplit  15762  sumsplit  15789  fprodsplit  15987  rpnnen2lem12  16248  sumeven  16411  sumodd  16412  saddisjlem  16488  lcmfunsnlem1  16661  lcmfunsnlem2lem1  16662  lcmfunsnlem2lem2  16663  lcmfunsnlem2  16664  coprmprod  16685  coprmproddvdslem  16686  nnnn0modprm0  16831  prm23lt5  16839  vdwapun  16999  ramubcl  17043  basprssdmsets  17245  mreexmrid  17660  lubun  18530  smndex1basss  18888  smndex1mgm  18890  smndex1mndlem  18892  smndex1n0mnd  18895  symgextf1  19407  gsumzsplit  19913  gsumzunsnd  19942  gsumunsnfd  19943  dprddisj2  20027  dmdprdsplit2lem  20033  dmdprdsplit2  20034  dprdsplit  20036  cnfldfun  21334  cnfldfunOLD  21347  mplcoe1  22000  mplcoe5  22003  evlslem4  22039  mdetunilem9  22563  maducoeval2  22583  madugsum  22586  clslp  23091  islpi  23092  restntr  23125  pnfnei  23163  mnfnei  23164  iunconn  23371  refun0  23458  xkoptsub  23597  ptunhmeo  23751  fbun  23783  filconn  23826  fixufil  23865  ufildr  23874  alexsubALTlem2  23991  alexsubALTlem3  23992  alexsubALTlem4  23993  tsmssplit  24095  xrtgioo  24751  reconnlem2  24772  iccpnfcnv  24898  iccpnfhmeo  24899  rrxcph  25349  rrxdstprj1  25366  mbfss  25604  mbfmax  25607  itg2splitlem  25706  itg2split  25707  iblss2  25764  itgsplit  25794  limcdif  25834  ellimc2  25835  limcmpt  25841  limcres  25844  limccnp  25849  limccnp2  25850  limcco  25851  rollelem  25950  dvivthlem1  25970  dvne0  25973  lhop  25978  degltlem1  26034  ply1rem  26128  fta1glem2  26131  plypf1  26174  plyaddlem1  26175  plymullem1  26176  plycj  26240  plycjOLD  26242  ofmulrt  26246  taylfval  26323  abelthlem2  26399  abelthlem3  26400  reasinsin  26863  scvxcvx  26953  ppinprm  27119  chtnprm  27121  dchrfi  27223  lgsdir2  27298  2lgslem3  27372  2lgsoddprmlem3  27382  nosepdmlem  27652  ssltun1  27777  ssltun2  27778  addsproplem2  27934  addsuniflem  27965  negsid  28004  mulsproplem9  28084  ssltmul1  28107  ssltmul2  28108  precsexlem9  28174  precsexlem11  28176  sltonold  28219  usgrexmplef  29243  cffldtocusgr  29431  cffldtocusgrOLD  29432  vtxdun  29466  eucrct2eupth  30231  shunssi  31354  atomli  32368  atoml2i  32369  rmoun  32480  rmounid  32481  nelun  32499  suppovss  32663  isoun  32684  fzsplit3  32775  eliccioo  32910  chnccats1  33000  gsumwun  33064  cycpmco2  33149  cyc3co2  33156  cycpmrn  33159  elrgspnlem2  33243  ply1dg3rt0irred  33600  lindsun  33670  lbsdiflsp0  33671  ordtconnlem1  33960  xrge0iifcnv  33969  xrge0iifiso  33971  xrge0iifhom  33973  esumsplit  34089  esumpad2  34092  measvuni  34250  sxbrsigalem0  34308  bnj1138  34824  bnj1137  35031  subfacp1lem4  35210  subfacp1lem5  35211  kur14lem7  35239  satfvsucsuc  35392  satfrnmapom  35397  satf0op  35404  satf0n0  35405  sat1el2xp  35406  fmlafvel  35412  isfmlasuc  35415  fmlaomn0  35417  satfv1fvfmla1  35450  2goelgoanfmla1  35451  mrsubcv  35537  mclsax  35596  brcup  35962  refssfne  36381  bj-eltag  37000  bj-0eltag  37001  bj-sngltag  37006  bj-projun  37017  bj-axbun  37059  bj-axadj  37064  bj-imdirco  37213  tan2h  37641  poimirlem2  37651  poimirlem8  37657  poimirlem18  37667  poimirlem21  37670  poimirlem22  37671  poimirlem23  37672  poimirlem24  37673  poimirlem25  37674  poimirlem27  37676  poimirlem29  37678  poimirlem31  37680  poimirlem32  37681  ftc1anclem1  37722  ftc1anclem5  37726  dvasin  37733  dvacos  37734  smprngopr  38081  elpadd  39823  paddval0  39834  hdmaplem4  41798  mapdh9a  41813  unitscyglem2  42214  ofun  42254  lzunuz  42766  jm2.23  42995  unxpwdom3  43094  hbtlem5  43127  fzunt  43454  fzuntd  43455  fzunt1d  43456  fzuntgd  43457  rp-fakeinunass  43514  sqrtcvallem1  43630  frege133d  43764  frege83  43945  frege131  43993  frege133  43995  uneqsn  44024  clsk1indlem3  44042  ntrneixb  44094  ntrneix3  44096  ntrneix13  44098  radcnvrat  44313  bccbc  44344  undif3VD  44881  iunconnlem2  44934  permaxinf2lem  45012  fnchoice  45033  limciccioolb  45630  limcicciooub  45646  icccncfext  45896  cncfiooicclem1  45902  fourierdlem70  46185  fourierdlem80  46195  fourierdlem93  46208  fourierdlem101  46216  sge0split  46418  el1fzopredsuc  47334  iccpartltu  47419  iccpartgtl  47420  iccpartgt  47421  iccpartleu  47422  iccpartgel  47423  fmtno4prmfac  47566  31prm  47591  sbgoldbo  47781  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  bgoldbtbndlem3  47801  bgoldbtbnd  47803  elclnbgrelnbgr  47819  clnbgrel  47822  clnbupgrel  47828  dfclnbgr6  47849  isubgr3stgrlem4  47961  usgrexmpl1tri  48009  usgrexmpl2nb0  48015  usgrexmpl2nb1  48016  usgrexmpl2nb2  48017  usgrexmpl2nb3  48018  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021  gpgprismgr4cycllem3  48076  gpgprismgr4cycllem7  48080  gpgprismgr4cycllem10  48083