Theorem elun 4147

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 3481	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3481	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3481	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 855	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2813	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2813	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 916	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3951	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3667	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 377	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 205   ∨ wo 845   = wceq 1533   ∈ wcel 2098  Vcvv 3461   ∪ cun 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-un 3951

This theorem is referenced by:  elunnel1  4148  elunnel2  4149  uneqri  4150  uncom  4152  uneq1  4155  nfun  4164  unass  4166  ssun1  4172  elunant  4178  unss1  4179  ssequn1  4180  rexun  4190  elsymdif  4248  indi  4274  undi  4275  unineq  4278  undif3  4291  rabun2  4315  reuun2  4316  undif4  4470  ssundif  4491  dfpr2  4652  elpwunsn  4691  eltpg  4693  pwpr  4906  pwtp  4907  uniun  4937  iinun2  5080  iunun  5100  iunxun  5101  iinuni  5105  brun  5203  pwssun  5576  opthprc  5745  xpundi  5749  xpundir  5750  difxp  6174  sossfld  6196  elsuci  6442  elsucg  6443  elsuc2g  6444  funun  6604  mptun  6706  unima  6976  eqfnun  7049  unpreima  7075  sucexeloniOLD  7818  suceloniOLD  7820  ordsucun  7833  fnse  8146  xpord2pred  8158  xpord3pred  8165  suppofssd  8217  reldmtpos  8248  dftpos4  8259  tpostpos  8260  frrlem12  8311  frrlem13  8312  wfrlem14OLD  8351  wfrlem15OLD  8352  oarec  8591  brdom2  9012  unfi  9209  unxpdomlem3  9289  domunfican  9358  dfsup2  9483  wemapso2lem  9591  unwdomg  9623  unxpwdom2  9627  cantnfp1lem3  9719  rankunb  9889  djur  9958  djuunxp  9960  eldju2ndl  9963  eldju2ndr  9964  djuun  9965  iscard3  10132  kmlem2  10190  ssfin4  10349  dffin7-2  10437  fin1a2lem11  10449  fin1a2lem12  10450  cfpwsdom  10623  elgch  10661  fpwwe2lem12  10681  canthp1lem2  10692  gch2  10714  elnn0  12521  un0addcl  12552  un0mulcl  12553  elxnn0  12593  ltxr  13144  elxr  13145  xrsupexmnf  13333  xrinfmexpnf  13334  supxrun  13344  ixxun  13389  difreicc  13510  iccsplit  13511  fzsplit2  13575  elfzp1  13600  uzsplit  13622  elfzp12  13629  fzosplit  13714  fzouzsplit  13716  elfzonlteqm1  13757  elfzo0l  13771  fzosplitsni  13793  elfzr  13795  elfzlmr  13796  hashnn0pnf  14354  hashf1lem2  14470  hash2pwpr  14490  pr2pwpr  14493  ccatrn  14592  cats1un  14724  fsumsplit  15740  sumsplit  15767  fprodsplit  15963  rpnnen2lem12  16222  sumeven  16384  sumodd  16385  saddisjlem  16459  lcmfunsnlem1  16633  lcmfunsnlem2lem1  16634  lcmfunsnlem2lem2  16635  lcmfunsnlem2  16636  coprmprod  16657  coprmproddvdslem  16658  nnnn0modprm0  16803  prm23lt5  16811  vdwapun  16971  ramubcl  17015  basprssdmsets  17221  mreexmrid  17651  lubun  18535  smndex1basss  18890  smndex1mgm  18892  smndex1mndlem  18894  smndex1n0mnd  18897  symgextf1  19414  gsumzsplit  19920  gsumzunsnd  19949  gsumunsnfd  19950  dprddisj2  20034  dmdprdsplit2lem  20040  dmdprdsplit2  20041  dprdsplit  20043  cnfldfun  21349  cnfldfunOLD  21362  mplcoe1  22036  mplcoe5  22039  evlslem4  22081  mdetunilem9  22605  maducoeval2  22625  madugsum  22628  clslp  23135  islpi  23136  restntr  23169  pnfnei  23207  mnfnei  23208  iunconn  23415  refun0  23502  xkoptsub  23641  ptunhmeo  23795  fbun  23827  filconn  23870  fixufil  23909  ufildr  23918  alexsubALTlem2  24035  alexsubALTlem3  24036  alexsubALTlem4  24037  tsmssplit  24139  xrtgioo  24805  reconnlem2  24826  iccpnfcnv  24952  iccpnfhmeo  24953  rrxcph  25403  rrxdstprj1  25420  mbfss  25658  mbfmax  25661  itg2splitlem  25761  itg2split  25762  iblss2  25818  itgsplit  25848  limcdif  25888  ellimc2  25889  limcmpt  25895  limcres  25898  limccnp  25903  limccnp2  25904  limcco  25905  rollelem  26004  dvivthlem1  26024  dvne0  26027  lhop  26032  degltlem1  26091  ply1rem  26185  fta1glem2  26188  plypf1  26231  plyaddlem1  26232  plymullem1  26233  plycj  26297  ofmulrt  26301  taylfval  26378  abelthlem2  26454  abelthlem3  26455  reasinsin  26916  scvxcvx  27006  ppinprm  27172  chtnprm  27174  dchrfi  27276  lgsdir2  27351  2lgslem3  27425  2lgsoddprmlem3  27435  nosepdmlem  27705  ssltun1  27830  ssltun2  27831  addsproplem2  27976  addsuniflem  28007  negsid  28042  mulsproplem9  28117  ssltmul1  28140  ssltmul2  28141  precsexlem9  28206  precsexlem11  28208  sltonold  28246  usgrexmplef  29187  cffldtocusgr  29375  cffldtocusgrOLD  29376  vtxdun  29410  eucrct2eupth  30170  shunssi  31293  atomli  32307  atoml2i  32308  rmoun  32413  rmounid  32414  elunsn  32429  nelun  32430  suppovss  32588  isoun  32604  fzsplit3  32685  eliccioo  32781  cycpmco2  32988  cyc3co2  32995  cycpmrn  32998  ply1dg3rt0irred  33429  lindsun  33492  lbsdiflsp0  33493  ordtconnlem1  33695  xrge0iifcnv  33704  xrge0iifiso  33706  xrge0iifhom  33708  esumsplit  33842  esumpad2  33845  measvuni  34003  sxbrsigalem0  34061  bnj1138  34589  bnj1137  34796  subfacp1lem4  34963  subfacp1lem5  34964  kur14lem7  34992  satfvsucsuc  35145  satfrnmapom  35150  satf0op  35157  satf0n0  35158  sat1el2xp  35159  fmlafvel  35165  isfmlasuc  35168  fmlaomn0  35170  satfv1fvfmla1  35203  2goelgoanfmla1  35204  mrsubcv  35290  mclsax  35349  brcup  35711  refssfne  36018  bj-eltag  36632  bj-0eltag  36633  bj-sngltag  36638  bj-projun  36649  bj-axbun  36691  bj-axadj  36696  bj-imdirco  36845  tan2h  37261  poimirlem2  37271  poimirlem8  37277  poimirlem18  37287  poimirlem21  37290  poimirlem22  37291  poimirlem23  37292  poimirlem24  37293  poimirlem25  37294  poimirlem27  37296  poimirlem29  37298  poimirlem31  37300  poimirlem32  37301  ftc1anclem1  37342  ftc1anclem5  37346  dvasin  37353  dvacos  37354  smprngopr  37701  elpadd  39446  paddval0  39457  hdmaplem4  41421  mapdh9a  41436  ofun  41903  lzunuz  42362  jm2.23  42591  unxpwdom3  42693  hbtlem5  42726  fzunt  43059  fzuntd  43060  fzunt1d  43061  fzuntgd  43062  rp-fakeinunass  43119  sqrtcvallem1  43235  frege133d  43369  frege83  43550  frege131  43598  frege133  43600  uneqsn  43629  clsk1indlem3  43647  ntrneixb  43699  ntrneix3  43701  ntrneix13  43703  radcnvrat  43925  bccbc  43956  undif3VD  44495  iunconnlem2  44548  fnchoice  44565  limciccioolb  45179  limcicciooub  45195  icccncfext  45445  cncfiooicclem1  45451  fourierdlem70  45734  fourierdlem80  45744  fourierdlem93  45757  fourierdlem101  45765  sge0split  45967  el1fzopredsuc  46875  iccpartltu  46934  iccpartgtl  46935  iccpartgt  46936  iccpartleu  46937  iccpartgel  46938  fmtno4prmfac  47081  31prm  47106  sbgoldbo  47296  nnsum4primeseven  47309  nnsum4primesevenALTV  47310  wtgoldbnnsum4prm  47311  bgoldbnnsum3prm  47313  bgoldbtbndlem3  47316  bgoldbtbnd  47318  clnbgrel  47336  clnbupgrel  47342  dfclnbgr6  47360