Theorem elun 3753

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 3212	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3212	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3212	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 394	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2689	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2689	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 746	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3579	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3353	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 368	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 196   ∨ wo 383   = wceq 1483   ∈ wcel 1990  Vcvv 3200   ∪ cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579

This theorem is referenced by:  elunnel1  3754  uneqri  3755  uncom  3757  uneq1  3760  unass  3770  ssun1  3776  unss1  3782  ssequn1  3783  unss  3787  rexun  3793  ralunb  3794  elsymdif  3849  symdif2  3852  indi  3873  undi  3874  unineq  3877  undif3  3888  undif3OLD  3889  rabun2  3906  reuun2  3910  undif4  4035  ssundif  4052  dfpr2  4195  elpwunsn  4224  eltpg  4227  pwpr  4430  pwtp  4431  uniun  4456  intun  4509  iinun2  4586  iunun  4604  iunxun  4605  iinuni  4609  brun  4703  pwunss  5019  pwssun  5020  opthprc  5167  xpundi  5171  xpundir  5172  difxp  5558  sossfld  5580  elsuci  5791  elsucg  5792  elsuc2g  5793  funun  5932  mptun  6025  unpreima  6341  suceloni  7013  ordsucun  7025  fnse  7294  reldmtpos  7360  dftpos4  7371  tpostpos  7372  wfrlem14  7428  wfrlem15  7429  oarec  7642  brdom2  7985  unxpdomlem3  8166  domunfican  8233  dfsup2  8350  wemapso2lem  8457  unwdomg  8489  unxpwdom2  8493  cantnfp1lem3  8577  rankunb  8713  iscard3  8916  kmlem2  8973  ssfin4  9132  dffin7-2  9220  fin1a2lem11  9232  fin1a2lem12  9233  cfpwsdom  9406  elgch  9444  fpwwe2lem13  9464  canthp1lem2  9475  gch2  9497  elnn0  11294  un0addcl  11326  un0mulcl  11327  elxnn0  11365  ltxr  11949  elxr  11950  xrsupexmnf  12135  xrinfmexpnf  12136  supxrun  12146  ixxun  12191  difreicc  12304  iccsplit  12305  fzsplit2  12366  elfzp1  12391  uzsplit  12412  elfzp12  12419  fzosplit  12501  fzouzsplit  12503  elfzonlteqm1  12543  elfzo0l  12558  fzosplitsni  12579  elfzr  12581  elfzlmr  12582  hashnn0pnf  13130  hashf1lem2  13240  hash2pwpr  13258  pr2pwpr  13261  ccatrn  13372  cats1un  13475  fsumsplit  14471  sumsplit  14499  fprodsplit  14696  rpnnen2lem12  14954  sumeven  15110  sumodd  15111  saddisjlem  15186  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  lcmfunsnlem2  15353  coprmprod  15375  coprmproddvdslem  15376  nnnn0modprm0  15511  prm23lt5  15519  vdwapun  15678  ramubcl  15722  basprssdmsets  15925  xpsfrnel2  16225  mreexmrid  16303  lubun  17123  symgextf1  17841  gsumzsplit  18327  gsumzunsnd  18355  gsumunsnfd  18356  dprddisj2  18438  dmdprdsplit2lem  18444  dmdprdsplit2  18445  dprdsplit  18447  mplcoe1  19465  mplcoe5  19468  evlslem4  19508  cnfldfunALT  19759  mdetunilem9  20426  maducoeval2  20446  madugsum  20449  clslp  20952  islpi  20953  restntr  20986  pnfnei  21024  mnfnei  21025  iunconn  21231  refun0  21318  xkoptsub  21457  ptunhmeo  21611  fbun  21644  filconn  21687  fixufil  21726  ufildr  21735  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  tsmssplit  21955  xrtgioo  22609  reconnlem2  22630  iccpnfcnv  22743  iccpnfhmeo  22744  rrxcph  23180  rrxdstprj1  23192  mbfss  23413  mbfmax  23416  itg2splitlem  23515  itg2split  23516  iblss2  23572  itgsplit  23602  limcdif  23640  ellimc2  23641  limcmpt  23647  limcres  23650  limccnp  23655  limccnp2  23656  limcco  23657  rollelem  23752  dvivthlem1  23771  dvne0  23774  lhop  23779  degltlem1  23832  ply1rem  23923  fta1glem2  23926  plypf1  23968  plyaddlem1  23969  plymullem1  23970  plycj  24033  ofmulrt  24037  taylfval  24113  abelthlem2  24186  abelthlem3  24187  reasinsin  24623  scvxcvx  24712  ppinprm  24878  chtnprm  24880  dchrfi  24980  lgsdir2  25055  2lgslem3  25129  2lgsoddprmlem3  25139  usgrexmplef  26151  cffldtocusgr  26343  vtxdun  26377  eucrct2eupth  27105  shunssi  28227  atomli  29241  atoml2i  29242  isoun  29479  fzsplit3  29553  eliccioo  29639  ordtconnlem1  29970  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhom  29983  esumsplit  30115  esumpad2  30118  measvuni  30277  sxbrsigalem0  30333  bnj1138  30859  bnj1137  31063  subfacp1lem4  31165  subfacp1lem5  31166  kur14lem7  31194  mrsubcv  31407  mclsax  31466  dftrpred3g  31733  nosepdmlem  31833  brcup  32046  refssfne  32353  bj-eltag  32965  bj-0eltag  32966  bj-sngltag  32971  bj-projun  32982  tan2h  33401  poimirlem2  33411  poimirlem8  33417  poimirlem18  33427  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem27  33436  poimirlem29  33438  poimirlem31  33440  poimirlem32  33441  ftc1anclem1  33485  ftc1anclem5  33489  dvasin  33496  dvacos  33497  eqfnun  33516  smprngopr  33851  elpadd  35085  paddval0  35096  hdmaplem4  37063  mapdh9a  37079  lzunuz  37331  jm2.23  37563  unxpwdom3  37665  hbtlem5  37698  rp-fakeinunass  37861  frege133d  38057  frege83  38240  frege131  38288  frege133  38290  uneqsn  38321  clsk1indlem3  38341  ntrneixb  38393  ntrneix3  38395  ntrneix13  38397  radcnvrat  38513  bccbc  38544  undif3VD  39118  iunconnlem2  39171  fnchoice  39188  elunnel2  39198  unima  39346  limciccioolb  39853  limcicciooub  39869  icccncfext  40100  cncfiooicclem1  40106  fourierdlem70  40393  fourierdlem80  40403  fourierdlem93  40416  fourierdlem101  40424  sge0split  40626  el1fzopredsuc  41335  iccpartltu  41361  iccpartgtl  41362  iccpartgt  41363  iccpartleu  41364  iccpartgel  41365  fmtno4prmfac  41484  31prm  41512  sbgoldbo  41675  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  bgoldbtbndlem3  41695  bgoldbtbnd  41697