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 3474	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3474	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3474	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 871	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2850	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2850	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 932	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3907	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3637	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   = wceq 1570   ∈ wcel 2145  Vcvv 3453   ∪ cun 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907

This theorem is used by:  elunnel1  4104  elunnel2  4105  uneqri  4106  uncom  4108  uneq1  4111  nfun  4120  unass  4121  ssun1  4127  elunant  4133  unss1  4134  ssequn1  4135  rexun  4145  elsymdif  4207  indi  4233  undi  4234  unineq  4237  undif3  4249  rabun2  4273  reuun2  4274  undif4  4423  ssundif  4446  dfpr2  4608  elunsn  4647  elpwunsn  4648  eltpg  4650  el7g  4654  pwpr  4864  pwtp  4865  uniun  4893  iinun2  5035  iunun  5057  iunxun  5058  iinuni  5062  brun  5160  trun  5227  pwssun  5551  opthprc  5723  xpundi  5728  xpundir  5729  difxp  6160  sossfld  6183  imadifssran  6201  imadifssranOLD  6202  elsuci  6431  elsucg  6432  elsuc2g  6433  funun  6583  mptun  6682  unima  6957  eqfnun  7033  unpreima  7059  ordsucun  7825  resf1extb  7935  fnse  8135  xpord2pred  8147  xpord3pred  8154  suppofssd  8205  reldmtpos  8236  dftpos4  8247  tpostpos  8248  frrlem12  8300  frrlem13  8301  oarec  8553  brdom2  8992  unfi  9169  unxpdomlem3  9232  domunfican  9295  dfsup2  9418  wemapso2lem  9528  unwdomg  9560  unxpwdom2  9564  cantnfp1lem3  9663  rankunb  9836  djur  9928  djuunxp  9930  eldju2ndl  9933  eldju2ndr  9934  djuun  9935  iscard3  10100  kmlem2  10158  ssfin4  10316  dffin7-2  10404  fin1a2lem11  10416  fin1a2lem12  10417  cfpwsdom  10597  elgch  10635  fpwwe2lem12  10655  canthp1lem2  10666  gch2  10688  elnn0  12534  un0addcl  12565  un0mulcl  12566  elxnn0  12607  ltxr  13170  elxr  13171  xrsupexmnf  13361  xrinfmexpnf  13362  supxrun  13372  ixxun  13418  difreicc  13541  iccsplit  13542  fzsplit2  13608  elfzp1  13633  uzsplit  13655  elfzp12  13662  fzosplit  13752  fzouzsplit  13754  elfzonlteqm1  13801  elfzo0l  13816  fzosplitsni  13839  elfzr  13841  elfzlmr  13842  hashnn0pnf  14410  hashf1lem2  14525  hash2pwpr  14545  pr2pwpr  14548  ccatrn  14659  cats1un  14794  fsumsplit  15831  sumsplit  15858  fprodsplit  16059  rpnnen2lem12  16319  sumeven  16483  sumodd  16484  saddisjlem  16560  lcmfunsnlem1  16733  lcmfunsnlem2lem1  16734  lcmfunsnlem2lem2  16735  lcmfunsnlem2  16736  coprmprod  16757  coprmproddvdslem  16758  nnnn0modprm0  16904  prm23lt5  16912  vdwapun  17072  ramubcl  17116  basprssdmsets  17319  mreexmrid  17737  lubun  18609  chnccats1  18719  smndex1basss  19023  smndex1mgm  19025  smndex1mndlem  19027  smndex1n0mnd  19030  symgextf1  19554  gsumzsplit  20060  gsumzunsnd  20089  gsumunsnfd  20090  dprddisj2  20174  dmdprdsplit2lem  20180  dmdprdsplit2  20181  dprdsplit  20183  cnfldfun  21605  mplcoe1  22259  mplcoe5  22262  evlslem4  22298  mdetunilem9  22848  maducoeval2  22868  madugsum  22871  clslp  23379  islpi  23380  restntr  23413  pnfnei  23451  mnfnei  23452  iunconn  23659  refun0  23747  xkoptsub  23886  ptunhmeo  24040  fbun  24072  filconn  24115  fixufil  24154  ufildr  24163  alexsubALTlem2  24280  alexsubALTlem3  24281  alexsubALTlem4  24282  tsmssplit  24384  xrtgioo  25039  reconnlem2  25060  iccpnfcnv  25178  iccpnfhmeo  25179  rrxcph  25626  rrxdstprj1  25643  mbfss  25880  mbfmax  25883  itg2splitlem  25982  itg2split  25983  iblss2  26040  itgsplit  26070  limcdif  26110  ellimc2  26111  limcmpt  26117  limcres  26120  limccnp  26125  limccnp2  26126  limcco  26127  rollelem  26223  dvivthlem1  26242  dvne0  26245  lhop  26250  degltlem1  26304  ply1rem  26398  fta1glem2  26401  plypf1  26445  plyaddlem1  26446  plymullem1  26447  plycj  26510  plycjOLD  26512  ofmulrt  26516  taylfval  26602  abelthlem2  26675  abelthlem3  26676  reasinsin  27141  scvxcvx  27230  ppinprm  27396  chtnprm  27398  dchrfi  27499  lgsdir2  27574  2lgslem3  27648  2lgsoddprmlem3  27658  nosepdmlem  27927  sltsun1  28061  sltsun2  28062  addsproplem2  28243  addsuniflem  28274  negsid  28314  mulsproplem9  28397  sltmuls1  28420  sltmuls2  28421  precsexlem9  28488  precsexlem11  28490  ltonold  28534  usgrexmplef  29727  cffldtocusgr  29915  vtxdun  29949  eucrct2eupth  30733  shunssi  31857  atomli  32871  atoml2i  32872  rmoun  32977  rmounid  32978  nelun  32996  suppovss  33161  isoun  33182  fzsplit3  33272  eliccioo  33384  gsumwun  33524  cycpmco2  33581  cyc3co2  33588  cycpmrn  33591  elrgspnlem2  33691  ply1dg3rt0irred  34002  lindsun  34143  lbsdiflsp0  34144  ordtconnlem1  34442  xrge0iifcnv  34451  xrge0iifiso  34453  xrge0iifhom  34455  esumsplit  34571  esumpad2  34574  measvuni  34733  sxbrsigalem0  34790  bnj1138  35306  bnj1137  35512  subfacp1lem4  35770  subfacp1lem5  35771  kur14lem7  35799  satfvsucsuc  35952  satfrnmapom  35957  satf0op  35964  satf0n0  35965  sat1el2xp  35966  fmlafvel  35972  isfmlasuc  35975  fmlaomn0  35977  satfv1fvfmla1  36010  2goelgoanfmla1  36011  mrsubcv  36097  mclsax  36156  brcup  36524  refssfne  36985  ttciunun  37138  bj-eltag  37729  bj-0eltag  37730  bj-sngltag  37735  bj-projun  37746  bj-axbun  37788  bj-axadj  37793  bj-imdirco  37950  tan2h  38374  poimirlem2  38379  poimirlem8  38385  poimirlem18  38395  poimirlem21  38398  poimirlem22  38399  poimirlem23  38400  poimirlem24  38401  poimirlem25  38402  poimirlem27  38404  poimirlem29  38406  poimirlem31  38408  poimirlem32  38409  ftc1anclem1  38450  ftc1anclem5  38454  dvasin  38461  dvacos  38462  smprngopr  38810  dfsucmap3  39219  elpadd  40680  paddval0  40691  hdmaplem4  42655  mapdh9a  42670  unitscyglem2  43070  ofun  43113  lzunuz  43621  jm2.23  43845  unxpwdom3  43944  hbtlem5  43977  fzunt  44303  fzuntd  44304  fzunt1d  44305  fzuntgd  44306  rp-fakeinunass  44363  sqrtcvallem1  44479  frege133d  44613  frege83  44794  frege131  44842  frege133  44844  uneqsn  44873  clsk1indlem3  44891  ntrneixb  44943  ntrneix3  44945  ntrneix13  44947  radcnvrat  45146  bccbc  45177  undif3VD  45712  iunconnlem2  45765  permaxinf2lem  45843  fnchoice  45871  limciccioolb  46459  limcicciooub  46473  icccncfext  46723  cncfiooicclem1  46729  fourierdlem70  47012  fourierdlem80  47022  fourierdlem93  47035  fourierdlem101  47043  sge0split  47245  wrddun2  47726  chndun2  47731  chnrun2  47736  el1fzopredsuc  48222  iccpartltu  48333  iccpartgtl  48334  iccpartgt  48335  iccpartleu  48336  iccpartgel  48337  fmtno4prmfac  48483  31prm  48508  sbgoldbo  48711  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  wtgoldbnnsum4prm  48726  bgoldbnnsum3prm  48728  bgoldbtbndlem3  48731  bgoldbtbnd  48733  elclnbgrelnbgr  48749  clnbgrel  48752  clnbupgrel  48758  dfclnbgr6  48780  isubgr3stgrlem4  48893  usgrexmpl1tri  48949  usgrexmpl2nb0  48955  usgrexmpl2nb1  48956  usgrexmpl2nb2  48957  usgrexmpl2nb3  48958  usgrexmpl2nb4  48959  usgrexmpl2nb5  48960  usgrexmpl2trifr  48961  gpgprismgr4cycllem3  49021  gpgprismgr4cycllem7  49025  gpgprismgr4cycllem10  49028  smprngprmrng  49262