Theorem elun 4103

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

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1541   ∈ wcel 2111  Vcvv 3436   ∪ cun 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907

This theorem is referenced by:  elunnel1  4104  elunnel2  4105  uneqri  4106  uncom  4108  uneq1  4111  nfun  4120  unass  4122  ssun1  4128  elunant  4134  unss1  4135  ssequn1  4136  rexun  4146  elsymdif  4208  indi  4234  undi  4235  unineq  4238  undif3  4250  rabun2  4274  reuun2  4275  undif4  4417  ssundif  4438  dfpr2  4597  elunsn  4636  elpwunsn  4637  eltpg  4639  el7g  4643  pwpr  4853  pwtp  4854  uniun  4882  iinun2  5021  iunun  5041  iunxun  5042  iinuni  5046  brun  5142  pwssun  5508  opthprc  5680  xpundi  5685  xpundir  5686  imadifssran  6098  difxp  6111  sossfld  6133  elsuci  6375  elsucg  6376  elsuc2g  6377  funun  6527  mptun  6627  unima  6897  eqfnun  6970  unpreima  6996  ordsucun  7755  resf1extb  7864  fnse  8063  xpord2pred  8075  xpord3pred  8082  suppofssd  8133  reldmtpos  8164  dftpos4  8175  tpostpos  8176  frrlem12  8227  frrlem13  8228  oarec  8477  brdom2  8904  unfi  9080  unxpdomlem3  9142  domunfican  9206  dfsup2  9328  wemapso2lem  9438  unwdomg  9470  unxpwdom2  9474  cantnfp1lem3  9570  rankunb  9740  djur  9809  djuunxp  9811  eldju2ndl  9814  eldju2ndr  9815  djuun  9816  iscard3  9981  kmlem2  10040  ssfin4  10198  dffin7-2  10286  fin1a2lem11  10298  fin1a2lem12  10299  cfpwsdom  10472  elgch  10510  fpwwe2lem12  10530  canthp1lem2  10541  gch2  10563  elnn0  12380  un0addcl  12411  un0mulcl  12412  elxnn0  12453  ltxr  13011  elxr  13012  xrsupexmnf  13201  xrinfmexpnf  13202  supxrun  13212  ixxun  13258  difreicc  13381  iccsplit  13382  fzsplit2  13446  elfzp1  13471  uzsplit  13493  elfzp12  13500  fzosplit  13589  fzouzsplit  13591  elfzonlteqm1  13638  elfzo0l  13653  fzosplitsni  13676  elfzr  13678  elfzlmr  13679  hashnn0pnf  14246  hashf1lem2  14360  hash2pwpr  14380  pr2pwpr  14383  ccatrn  14494  cats1un  14625  fsumsplit  15645  sumsplit  15672  fprodsplit  15870  rpnnen2lem12  16131  sumeven  16295  sumodd  16296  saddisjlem  16372  lcmfunsnlem1  16545  lcmfunsnlem2lem1  16546  lcmfunsnlem2lem2  16547  lcmfunsnlem2  16548  coprmprod  16569  coprmproddvdslem  16570  nnnn0modprm0  16715  prm23lt5  16723  vdwapun  16883  ramubcl  16927  basprssdmsets  17129  mreexmrid  17546  lubun  18418  chnccats1  18528  smndex1basss  18810  smndex1mgm  18812  smndex1mndlem  18814  smndex1n0mnd  18817  symgextf1  19331  gsumzsplit  19837  gsumzunsnd  19866  gsumunsnfd  19867  dprddisj2  19951  dmdprdsplit2lem  19957  dmdprdsplit2  19958  dprdsplit  19960  cnfldfun  21303  cnfldfunOLD  21316  mplcoe1  21970  mplcoe5  21973  evlslem4  22009  mdetunilem9  22533  maducoeval2  22553  madugsum  22556  clslp  23061  islpi  23062  restntr  23095  pnfnei  23133  mnfnei  23134  iunconn  23341  refun0  23428  xkoptsub  23567  ptunhmeo  23721  fbun  23753  filconn  23796  fixufil  23835  ufildr  23844  alexsubALTlem2  23961  alexsubALTlem3  23962  alexsubALTlem4  23963  tsmssplit  24065  xrtgioo  24720  reconnlem2  24741  iccpnfcnv  24867  iccpnfhmeo  24868  rrxcph  25317  rrxdstprj1  25334  mbfss  25572  mbfmax  25575  itg2splitlem  25674  itg2split  25675  iblss2  25732  itgsplit  25762  limcdif  25802  ellimc2  25803  limcmpt  25809  limcres  25812  limccnp  25817  limccnp2  25818  limcco  25819  rollelem  25918  dvivthlem1  25938  dvne0  25941  lhop  25946  degltlem1  26002  ply1rem  26096  fta1glem2  26099  plypf1  26142  plyaddlem1  26143  plymullem1  26144  plycj  26208  plycjOLD  26210  ofmulrt  26214  taylfval  26291  abelthlem2  26367  abelthlem3  26368  reasinsin  26831  scvxcvx  26921  ppinprm  27087  chtnprm  27089  dchrfi  27191  lgsdir2  27266  2lgslem3  27340  2lgsoddprmlem3  27350  nosepdmlem  27620  ssltun1  27747  ssltun2  27748  addsproplem2  27911  addsuniflem  27942  negsid  27981  mulsproplem9  28061  ssltmul1  28084  ssltmul2  28085  precsexlem9  28151  precsexlem11  28153  sltonold  28196  usgrexmplef  29235  cffldtocusgr  29423  cffldtocusgrOLD  29424  vtxdun  29458  eucrct2eupth  30220  shunssi  31343  atomli  32357  atoml2i  32358  rmoun  32468  rmounid  32469  nelun  32488  suppovss  32657  isoun  32678  fzsplit3  32771  eliccioo  32906  gsumwun  33040  cycpmco2  33097  cyc3co2  33104  cycpmrn  33107  elrgspnlem2  33205  ply1dg3rt0irred  33541  lindsun  33633  lbsdiflsp0  33634  ordtconnlem1  33932  xrge0iifcnv  33941  xrge0iifiso  33943  xrge0iifhom  33945  esumsplit  34061  esumpad2  34064  measvuni  34222  sxbrsigalem0  34279  bnj1138  34795  bnj1137  35002  subfacp1lem4  35215  subfacp1lem5  35216  kur14lem7  35244  satfvsucsuc  35397  satfrnmapom  35402  satf0op  35409  satf0n0  35410  sat1el2xp  35411  fmlafvel  35417  isfmlasuc  35420  fmlaomn0  35422  satfv1fvfmla1  35455  2goelgoanfmla1  35456  mrsubcv  35542  mclsax  35601  brcup  35972  refssfne  36391  bj-eltag  37010  bj-0eltag  37011  bj-sngltag  37016  bj-projun  37027  bj-axbun  37069  bj-axadj  37074  bj-imdirco  37223  tan2h  37651  poimirlem2  37661  poimirlem8  37667  poimirlem18  37677  poimirlem21  37680  poimirlem22  37681  poimirlem23  37682  poimirlem24  37683  poimirlem25  37684  poimirlem27  37686  poimirlem29  37688  poimirlem31  37690  poimirlem32  37691  ftc1anclem1  37732  ftc1anclem5  37736  dvasin  37743  dvacos  37744  smprngopr  38091  elpadd  39837  paddval0  39848  hdmaplem4  41812  mapdh9a  41827  unitscyglem2  42228  ofun  42268  lzunuz  42800  jm2.23  43028  unxpwdom3  43127  hbtlem5  43160  fzunt  43487  fzuntd  43488  fzunt1d  43489  fzuntgd  43490  rp-fakeinunass  43547  sqrtcvallem1  43663  frege133d  43797  frege83  43978  frege131  44026  frege133  44028  uneqsn  44057  clsk1indlem3  44075  ntrneixb  44127  ntrneix3  44129  ntrneix13  44131  radcnvrat  44346  bccbc  44377  undif3VD  44913  iunconnlem2  44966  permaxinf2lem  45044  fnchoice  45065  limciccioolb  45660  limcicciooub  45674  icccncfext  45924  cncfiooicclem1  45930  fourierdlem70  46213  fourierdlem80  46223  fourierdlem93  46236  fourierdlem101  46244  sge0split  46446  el1fzopredsuc  47355  iccpartltu  47455  iccpartgtl  47456  iccpartgt  47457  iccpartleu  47458  iccpartgel  47459  fmtno4prmfac  47602  31prm  47627  sbgoldbo  47817  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  wtgoldbnnsum4prm  47832  bgoldbnnsum3prm  47834  bgoldbtbndlem3  47837  bgoldbtbnd  47839  elclnbgrelnbgr  47855  clnbgrel  47858  clnbupgrel  47864  dfclnbgr6  47886  isubgr3stgrlem4  47999  usgrexmpl1tri  48055  usgrexmpl2nb0  48061  usgrexmpl2nb1  48062  usgrexmpl2nb2  48063  usgrexmpl2nb3  48064  usgrexmpl2nb4  48065  usgrexmpl2nb5  48066  usgrexmpl2trifr  48067  gpgprismgr4cycllem3  48127  gpgprismgr4cycllem7  48131  gpgprismgr4cycllem10  48134