Theorem elun 4093

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 3450	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3450	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3450	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 858	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2824	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2824	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 919	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3894	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3623	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 206   ∨ wo 848   = wceq 1542   ∈ wcel 2114  Vcvv 3429   ∪ cun 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894

This theorem is referenced by:  elunnel1  4094  elunnel2  4095  uneqri  4096  uncom  4098  uneq1  4101  nfun  4110  unass  4112  ssun1  4118  elunant  4124  unss1  4125  ssequn1  4126  rexun  4136  elsymdif  4198  indi  4224  undi  4225  unineq  4228  undif3  4240  rabun2  4264  reuun2  4265  undif4  4407  ssundif  4427  dfpr2  4588  elunsn  4627  elpwunsn  4628  eltpg  4630  el7g  4634  pwpr  4844  pwtp  4845  uniun  4873  iinun2  5015  iunun  5035  iunxun  5036  iinuni  5040  brun  5136  trun  5203  pwssun  5523  opthprc  5695  xpundi  5700  xpundir  5701  imadifssran  6115  difxp  6128  sossfld  6150  elsuci  6392  elsucg  6393  elsuc2g  6394  funun  6544  mptun  6644  unima  6915  eqfnun  6989  unpreima  7015  ordsucun  7776  resf1extb  7885  fnse  8083  xpord2pred  8095  xpord3pred  8102  suppofssd  8153  reldmtpos  8184  dftpos4  8195  tpostpos  8196  frrlem12  8247  frrlem13  8248  oarec  8497  brdom2  8929  unfi  9105  unxpdomlem3  9168  domunfican  9232  dfsup2  9357  wemapso2lem  9467  unwdomg  9499  unxpwdom2  9503  cantnfp1lem3  9601  rankunb  9774  djur  9843  djuunxp  9845  eldju2ndl  9848  eldju2ndr  9849  djuun  9850  iscard3  10015  kmlem2  10074  ssfin4  10232  dffin7-2  10320  fin1a2lem11  10332  fin1a2lem12  10333  cfpwsdom  10507  elgch  10545  fpwwe2lem12  10565  canthp1lem2  10576  gch2  10598  elnn0  12439  un0addcl  12470  un0mulcl  12471  elxnn0  12512  ltxr  13066  elxr  13067  xrsupexmnf  13257  xrinfmexpnf  13258  supxrun  13268  ixxun  13314  difreicc  13437  iccsplit  13438  fzsplit2  13503  elfzp1  13528  uzsplit  13550  elfzp12  13557  fzosplit  13647  fzouzsplit  13649  elfzonlteqm1  13696  elfzo0l  13711  fzosplitsni  13734  elfzr  13736  elfzlmr  13737  hashnn0pnf  14304  hashf1lem2  14418  hash2pwpr  14438  pr2pwpr  14441  ccatrn  14552  cats1un  14683  fsumsplit  15703  sumsplit  15730  fprodsplit  15931  rpnnen2lem12  16192  sumeven  16356  sumodd  16357  saddisjlem  16433  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  lcmfunsnlem2  16609  coprmprod  16630  coprmproddvdslem  16631  nnnn0modprm0  16777  prm23lt5  16785  vdwapun  16945  ramubcl  16989  basprssdmsets  17191  mreexmrid  17609  lubun  18481  chnccats1  18591  smndex1basss  18876  smndex1mgm  18878  smndex1mndlem  18880  smndex1n0mnd  18883  symgextf1  19396  gsumzsplit  19902  gsumzunsnd  19931  gsumunsnfd  19932  dprddisj2  20016  dmdprdsplit2lem  20022  dmdprdsplit2  20023  dprdsplit  20025  cnfldfun  21366  mplcoe1  22015  mplcoe5  22018  evlslem4  22054  mdetunilem9  22585  maducoeval2  22605  madugsum  22608  clslp  23113  islpi  23114  restntr  23147  pnfnei  23185  mnfnei  23186  iunconn  23393  refun0  23480  xkoptsub  23619  ptunhmeo  23773  fbun  23805  filconn  23848  fixufil  23887  ufildr  23896  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  tsmssplit  24117  xrtgioo  24772  reconnlem2  24793  iccpnfcnv  24911  iccpnfhmeo  24912  rrxcph  25359  rrxdstprj1  25376  mbfss  25613  mbfmax  25616  itg2splitlem  25715  itg2split  25716  iblss2  25773  itgsplit  25803  limcdif  25843  ellimc2  25844  limcmpt  25850  limcres  25853  limccnp  25858  limccnp2  25859  limcco  25860  rollelem  25956  dvivthlem1  25975  dvne0  25978  lhop  25983  degltlem1  26037  ply1rem  26131  fta1glem2  26134  plypf1  26177  plyaddlem1  26178  plymullem1  26179  plycj  26242  plycjOLD  26244  ofmulrt  26248  taylfval  26324  abelthlem2  26397  abelthlem3  26398  reasinsin  26860  scvxcvx  26949  ppinprm  27115  chtnprm  27117  dchrfi  27218  lgsdir2  27293  2lgslem3  27367  2lgsoddprmlem3  27377  nosepdmlem  27647  sltsun1  27780  sltsun2  27781  addsproplem2  27962  addsuniflem  27993  negsid  28033  mulsproplem9  28116  sltmuls1  28139  sltmuls2  28140  precsexlem9  28207  precsexlem11  28209  ltonold  28253  usgrexmplef  29328  cffldtocusgr  29516  vtxdun  29550  eucrct2eupth  30315  shunssi  31439  atomli  32453  atoml2i  32454  rmoun  32563  rmounid  32564  nelun  32583  suppovss  32754  isoun  32775  fzsplit3  32866  eliccioo  32990  gsumwun  33137  cycpmco2  33194  cyc3co2  33201  cycpmrn  33204  elrgspnlem2  33304  ply1dg3rt0irred  33644  lindsun  33769  lbsdiflsp0  33770  ordtconnlem1  34068  xrge0iifcnv  34077  xrge0iifiso  34079  xrge0iifhom  34081  esumsplit  34197  esumpad2  34200  measvuni  34358  sxbrsigalem0  34415  bnj1138  34931  bnj1137  35137  subfacp1lem4  35365  subfacp1lem5  35366  kur14lem7  35394  satfvsucsuc  35547  satfrnmapom  35552  satf0op  35559  satf0n0  35560  sat1el2xp  35561  fmlafvel  35567  isfmlasuc  35570  fmlaomn0  35572  satfv1fvfmla1  35605  2goelgoanfmla1  35606  mrsubcv  35692  mclsax  35751  brcup  36119  refssfne  36540  ttciunun  36693  bj-eltag  37284  bj-0eltag  37285  bj-sngltag  37290  bj-projun  37301  bj-axbun  37343  bj-axadj  37348  bj-imdirco  37504  tan2h  37933  poimirlem2  37943  poimirlem8  37949  poimirlem18  37959  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem27  37968  poimirlem29  37970  poimirlem31  37972  poimirlem32  37973  ftc1anclem1  38014  ftc1anclem5  38018  dvasin  38025  dvacos  38026  smprngopr  38373  dfsucmap3  38784  elpadd  40245  paddval0  40256  hdmaplem4  42220  mapdh9a  42235  unitscyglem2  42635  ofun  42677  lzunuz  43200  jm2.23  43424  unxpwdom3  43523  hbtlem5  43556  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  rp-fakeinunass  43942  sqrtcvallem1  44058  frege133d  44192  frege83  44373  frege131  44421  frege133  44423  uneqsn  44452  clsk1indlem3  44470  ntrneixb  44522  ntrneix3  44524  ntrneix13  44526  radcnvrat  44741  bccbc  44772  undif3VD  45308  iunconnlem2  45361  permaxinf2lem  45439  fnchoice  45460  limciccioolb  46051  limcicciooub  46065  icccncfext  46315  cncfiooicclem1  46321  fourierdlem70  46604  fourierdlem80  46614  fourierdlem93  46627  fourierdlem101  46635  sge0split  46837  el1fzopredsuc  47774  iccpartltu  47885  iccpartgtl  47886  iccpartgt  47887  iccpartleu  47888  iccpartgel  47889  fmtno4prmfac  48035  31prm  48060  sbgoldbo  48263  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  bgoldbtbndlem3  48283  bgoldbtbnd  48285  elclnbgrelnbgr  48301  clnbgrel  48304  clnbupgrel  48310  dfclnbgr6  48332  isubgr3stgrlem4  48445  usgrexmpl1tri  48501  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  usgrexmpl2trifr  48513  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem7  48577  gpgprismgr4cycllem10  48580