Theorem elun 4152

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   = wceq 1569   ∈ wcel 2144  Vcvv 3450   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151

This theorem is used by:  elunnel1  4153  elunnel2  4154  uneqri  4155  uncom  4157  uneq1  4160  nfun  4169  unass  4170  ssun1  4176  elunant  4182  unss1  4183  ssequn1  4184  rexun  4194  elsymdif  4203  indi  4229  undi  4230  unineq  4233  undif3  4245  rabun2  4269  reuun2  4270  undif4  4419  ssundif  4442  dfpr2  4601  elunsn  4640  elpwunsn  4641  eltpg  4643  el7g  4647  pwpr  4827  pwtp  4828  uniun  4889  iinun2  5030  iunun  5052  iunxun  5053  iinuni  5057  brun  5155  trun  5222  pwssun  5542  opthprc  5714  xpundi  5719  xpundir  5720  difxp  6154  sossfld  6177  imadifssranOLD  6202  imadifssranOLDOLD  6203  elsuci  6432  elsucg  6433  elsuc2g  6434  funun  6586  mptun  6685  unima  6960  eqfnun  7036  unpreima  7062  ordsucun  7836  resf1extb  7946  fnse  8152  xpord2pred  8164  xpord3pred  8171  suppofssd  8223  reldmtpos  8254  dftpos4  8265  tpostpos  8266  frrlem12  8318  frrlem13  8319  oarec  8573  brdom2  9012  unfi  9189  unxpdomlem3  9252  domunfican  9316  dfsup2  9439  wemapso2lem  9549  unwdomg  9581  unxpwdom2  9585  cantnfp1lem3  9684  rankunb  9867  djur  10003  djuunxp  10005  eldju2ndl  10008  eldju2ndr  10009  djuun  10010  iscard3  10175  kmlem2  10233  ssfin4  10391  dffin7-2  10479  fin1a2lem11  10491  fin1a2lem12  10492  cfpwsdom  10672  elgch  10710  fpwwe2lem12  10730  canthp1lem2  10741  gch2  10763  elnn0  12611  un0addcl  12642  un0mulcl  12643  elxnn0  12684  ltxr  13247  elxr  13248  xrsupexmnf  13438  xrinfmexpnf  13439  supxrun  13449  ixxun  13495  difreicc  13618  iccsplit  13619  fzsplit2  13686  elfzp1  13711  uzsplit  13733  elfzp12  13740  fzosplit  13830  fzouzsplit  13832  elfzonlteqm1  13879  elfzo0l  13894  fzosplitsni  13917  elfzr  13919  elfzlmr  13920  hashnn0pnf  14489  hashf1lem2  14604  hash2pwpr  14624  pr2pwpr  14627  ccatrn  14738  cats1un  14874  fsumsplit  15912  sumsplit  15939  fprodsplit  16138  rpnnen2lem12  16398  sumeven  16562  sumodd  16563  saddisjlem  16639  lcmfunsnlem1  16817  lcmfunsnlem2lem1  16818  lcmfunsnlem2lem2  16819  lcmfunsnlem2  16820  coprmprod  16841  coprmproddvdslem  16842  nnnn0modprm0  16989  prm23lt5  16997  vdwapun  17157  ramubcl  17201  basprssdmsets  17404  mreexmrid  17822  lubun  18694  chnccats1  18804  smndex1basss  19109  smndex1mgm  19111  smndex1mndlem  19113  smndex1n0mnd  19116  symgextf1  19640  gsumzsplit  20146  gsumzunsnd  20175  gsumunsnfd  20176  dprddisj2  20260  dmdprdsplit2lem  20266  dmdprdsplit2  20267  dprdsplit  20269  cnfldfun  21697  mplcoe1  22351  mplcoe5  22354  evlslem4  22390  mdetunilem9  22940  maducoeval2  22960  madugsum  22963  clslp  23471  islpi  23472  restntr  23505  pnfnei  23543  mnfnei  23544  iunconn  23751  refun0  23839  xkoptsub  23978  ptunhmeo  24132  fbun  24164  filconn  24207  fixufil  24246  ufildr  24255  alexsubALTlem2  24372  alexsubALTlem3  24373  alexsubALTlem4  24374  tsmssplit  24476  xrtgioo  25131  reconnlem2  25152  iccpnfcnv  25270  iccpnfhmeo  25271  rrxcph  25718  rrxdstprj1  25735  mbfss  25972  mbfmax  25975  itg2splitlem  26074  itg2split  26075  iblss2  26131  itgsplit  26161  limcdif  26201  ellimc2  26202  limcmpt  26208  limcres  26211  limccnp  26216  limccnp2  26217  limcco  26218  rollelem  26314  dvivthlem1  26333  dvne0  26336  lhop  26341  degltlem1  26395  ply1rem  26489  fta1glem2  26492  plypf1  26536  plyaddlem1  26537  plymullem1  26538  plycj  26601  ofmulrt  26605  taylfval  26691  abelthlem2  26764  abelthlem3  26765  reasinsin  27229  scvxcvx  27318  ppinprm  27484  chtnprm  27486  dchrfi  27587  lgsdir2  27662  2lgslem3  27736  2lgsoddprmlem3  27746  nosepdmlem  28045  sltsun1  28179  sltsun2  28180  addsproplem2  28361  addsuniflem  28392  negsid  28432  mulsproplem9  28515  sltmuls1  28538  sltmuls2  28539  precsexlem9  28606  precsexlem11  28608  ltonold  28652  usgrexmplef  29845  cffldtocusgr  30033  vtxdun  30067  eucrct2eupth  30851  shunssi  31975  atomli  32989  atoml2i  32990  rmoun  33137  rmounid  33138  nelun  33156  suppovss  33321  isoun  33342  fzsplit3  33431  eliccioo  33543  gsumwun  33683  cycpmco2  33740  cyc3co2  33747  cycpmrn  33750  elrgspnlem2  33850  ply1dg3rt0irred  34162  lindsun  34303  lbsdiflsp0  34304  ordtconnlem1  34602  xrge0iifcnv  34611  xrge0iifiso  34613  xrge0iifhom  34615  esumsplit  34731  esumpad2  34734  measvuni  34893  sxbrsigalem0  34949  bnj1138  35465  bnj1137  35671  subfacp1lem4  36034  subfacp1lem5  36035  kur14lem7  36063  satfvsucsuc  36216  satfrnmapom  36221  satf0op  36228  satf0n0  36229  sat1el2xp  36230  fmlafvel  36236  isfmlasuc  36239  fmlaomn0  36241  satfv1fvfmla1  36274  2goelgoanfmla1  36275  mrsubcv  36361  mclsax  36420  brcup  36793  refssfne  37238  ttciunun  37391  bj-eltag  37982  bj-0eltag  37983  bj-sngltag  37988  bj-projun  37999  bj-axbun  38041  bj-axadj  38046  bj-imdirco  38204  tan2h  38628  poimirlem2  38633  poimirlem8  38639  poimirlem18  38649  poimirlem21  38652  poimirlem22  38653  poimirlem23  38654  poimirlem24  38655  poimirlem25  38656  poimirlem27  38658  poimirlem29  38660  poimirlem31  38662  poimirlem32  38663  ftc1anclem1  38704  ftc1anclem5  38708  dvasin  38715  dvacos  38716  smprngopr  39079  dfsucmap3  39488  elpadd  40949  paddval0  40960  hdmaplem4  42924  mapdh9a  42939  unitscyglem2  43339  ofun  43382  lzunuz  43872  jm2.23  44096  unxpwdom3  44190  hbtlem5  44223  fzunt  44549  fzuntd  44550  fzunt1d  44551  fzuntgd  44552  rp-fakeinunass  44609  sqrtcvallem1  44724  frege133d  44858  frege83  45039  frege131  45087  frege133  45089  uneqsn  45118  clsk1indlem3  45136  ntrneixb  45188  ntrneix3  45190  ntrneix13  45192  radcnvrat  45391  bccbc  45422  undif3VD  45957  iunconnlem2  46010  permaxinf2lem  46095  fnchoice  46139  limciccioolb  46726  limcicciooub  46740  icccncfext  46990  cncfiooicclem1  46996  fourierdlem70  47279  fourierdlem80  47289  fourierdlem93  47302  fourierdlem101  47310  sge0split  47512  wrddun2  47993  chndun2  47998  chnrun2  48003  el1fzopredsuc  48489  iccpartltu  48600  iccpartgtl  48601  iccpartgt  48602  iccpartleu  48603  iccpartgel  48604  fmtno4prmfac  48750  31prm  48775  sbgoldbo  48978  nnsum4primeseven  48991  nnsum4primesevenALTV  48992  wtgoldbnnsum4prm  48993  bgoldbnnsum3prm  48995  bgoldbtbndlem3  48998  bgoldbtbnd  49000  elclnbgrelnbgr  49016  clnbgrel  49019  clnbupgrel  49025  dfclnbgr6  49047  isubgr3stgrlem4  49160  usgrexmpl1tri  49216  usgrexmpl2nb0  49222  usgrexmpl2nb1  49223  usgrexmpl2nb2  49224  usgrexmpl2nb3  49225  usgrexmpl2nb4  49226  usgrexmpl2nb5  49227  usgrexmpl2trifr  49228  gpgprismgr4cycllem3  49288  gpgprismgr4cycllem7  49292  gpgprismgr4cycllem10  49295  smprngprmrng  49529  parhomcl2  50838