Theorem elun 4125

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 3512	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3512	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3512	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 853	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2900	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2900	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 915	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3941	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3668	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 382	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 208   ∨ wo 843   = wceq 1537   ∈ wcel 2114  Vcvv 3494   ∪ cun 3934

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941

This theorem is referenced by:  elunnel1  4126  uneqri  4127  uncom  4129  uneq1  4132  unass  4142  ssun1  4148  elunant  4154  unss1  4155  ssequn1  4156  rexun  4166  elsymdif  4224  indi  4250  undi  4251  unineq  4254  undif3  4265  rabun2  4282  reuun2  4286  undif4  4416  ssundif  4433  dfpr2  4586  elpwunsn  4621  eltpg  4623  pwpr  4832  pwtp  4833  uniun  4861  iinun2  4995  iunun  5015  iunxun  5016  iinuni  5020  brun  5117  pwunssOLD  5455  pwssun  5456  opthprc  5616  xpundi  5620  xpundir  5621  difxp  6021  sossfld  6043  elsuci  6257  elsucg  6258  elsuc2g  6259  funun  6400  mptun  6494  unima  6739  unpreima  6833  suceloni  7528  ordsucun  7540  fnse  7827  suppofssd  7867  reldmtpos  7900  dftpos4  7911  tpostpos  7912  wfrlem14  7968  wfrlem15  7969  oarec  8188  brdom2  8539  unxpdomlem3  8724  domunfican  8791  dfsup2  8908  wemapso2lem  9016  unwdomg  9048  unxpwdom2  9052  cantnfp1lem3  9143  rankunb  9279  djur  9348  djuunxp  9350  eldju2ndl  9353  eldju2ndr  9354  djuun  9355  iscard3  9519  kmlem2  9577  ssfin4  9732  dffin7-2  9820  fin1a2lem11  9832  fin1a2lem12  9833  cfpwsdom  10006  elgch  10044  fpwwe2lem13  10064  canthp1lem2  10075  gch2  10097  elnn0  11900  un0addcl  11931  un0mulcl  11932  elxnn0  11970  ltxr  12511  elxr  12512  xrsupexmnf  12699  xrinfmexpnf  12700  supxrun  12710  ixxun  12755  difreicc  12871  iccsplit  12872  fzsplit2  12933  elfzp1  12958  uzsplit  12980  elfzp12  12987  fzosplit  13071  fzouzsplit  13073  elfzonlteqm1  13114  elfzo0l  13128  fzosplitsni  13149  elfzr  13151  elfzlmr  13152  hashnn0pnf  13703  hashf1lem2  13815  hash2pwpr  13835  pr2pwpr  13838  ccatrn  13943  cats1un  14083  fsumsplit  15097  sumsplit  15123  fprodsplit  15320  rpnnen2lem12  15578  sumeven  15738  sumodd  15739  saddisjlem  15813  lcmfunsnlem1  15981  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  lcmfunsnlem2  15984  coprmprod  16005  coprmproddvdslem  16006  nnnn0modprm0  16143  prm23lt5  16151  vdwapun  16310  ramubcl  16354  basprssdmsets  16549  mreexmrid  16914  lubun  17733  smndex1basss  18070  smndex1mgm  18072  smndex1mndlem  18074  smndex1n0mnd  18077  symgextf1  18549  gsumzsplit  19047  gsumzunsnd  19076  gsumunsnfd  19077  dprddisj2  19161  dmdprdsplit2lem  19167  dmdprdsplit2  19168  dprdsplit  19170  mplcoe1  20246  mplcoe5  20249  evlslem4  20288  cnfldfunALT  20558  mdetunilem9  21229  maducoeval2  21249  madugsum  21252  clslp  21756  islpi  21757  restntr  21790  pnfnei  21828  mnfnei  21829  iunconn  22036  refun0  22123  xkoptsub  22262  ptunhmeo  22416  fbun  22448  filconn  22491  fixufil  22530  ufildr  22539  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALTlem4  22658  tsmssplit  22760  xrtgioo  23414  reconnlem2  23435  iccpnfcnv  23548  iccpnfhmeo  23549  rrxcph  23995  rrxdstprj1  24012  mbfss  24247  mbfmax  24250  itg2splitlem  24349  itg2split  24350  iblss2  24406  itgsplit  24436  limcdif  24474  ellimc2  24475  limcmpt  24481  limcres  24484  limccnp  24489  limccnp2  24490  limcco  24491  rollelem  24586  dvivthlem1  24605  dvne0  24608  lhop  24613  degltlem1  24666  ply1rem  24757  fta1glem2  24760  plypf1  24802  plyaddlem1  24803  plymullem1  24804  plycj  24867  ofmulrt  24871  taylfval  24947  abelthlem2  25020  abelthlem3  25021  reasinsin  25474  scvxcvx  25563  ppinprm  25729  chtnprm  25731  dchrfi  25831  lgsdir2  25906  2lgslem3  25980  2lgsoddprmlem3  25990  usgrexmplef  27041  cffldtocusgr  27229  vtxdun  27263  eucrct2eupth  28024  shunssi  29145  atomli  30159  atoml2i  30160  rmoun  30258  rmounid  30259  elunsn  30273  nelun  30274  suppovss  30426  isoun  30437  fzsplit3  30517  eliccioo  30607  cycpmco2  30775  cyc3co2  30782  cycpmrn  30785  lindsun  31021  lbsdiflsp0  31022  ordtconnlem1  31167  xrge0iifcnv  31176  xrge0iifiso  31178  xrge0iifhom  31180  esumsplit  31312  esumpad2  31315  measvuni  31473  sxbrsigalem0  31529  bnj1138  32060  bnj1137  32267  subfacp1lem4  32430  subfacp1lem5  32431  kur14lem7  32459  satfvsucsuc  32612  satfrnmapom  32617  satf0op  32624  satf0n0  32625  sat1el2xp  32626  fmlafvel  32632  isfmlasuc  32635  fmlaomn0  32637  satfv1fvfmla1  32670  2goelgoanfmla1  32671  mrsubcv  32757  mclsax  32816  dftrpred3g  33072  frrlem12  33134  frrlem13  33135  nosepdmlem  33187  brcup  33400  refssfne  33706  bj-eltag  34292  bj-0eltag  34293  bj-sngltag  34298  bj-projun  34309  tan2h  34899  poimirlem2  34909  poimirlem8  34915  poimirlem18  34925  poimirlem21  34928  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem27  34934  poimirlem29  34936  poimirlem31  34938  poimirlem32  34939  ftc1anclem1  34982  ftc1anclem5  34986  dvasin  34993  dvacos  34994  eqfnun  35012  smprngopr  35345  elpadd  36950  paddval0  36961  hdmaplem4  38925  mapdh9a  38940  lzunuz  39414  jm2.23  39642  unxpwdom3  39744  hbtlem5  39777  rp-fakeinunass  39930  frege133d  40159  frege83  40341  frege131  40389  frege133  40391  uneqsn  40422  clsk1indlem3  40442  ntrneixb  40494  ntrneix3  40496  ntrneix13  40498  radcnvrat  40695  bccbc  40726  undif3VD  41265  iunconnlem2  41318  fnchoice  41335  elunnel2  41345  limciccioolb  41951  limcicciooub  41967  icccncfext  42219  cncfiooicclem1  42225  fourierdlem70  42510  fourierdlem80  42520  fourierdlem93  42533  fourierdlem101  42541  sge0split  42740  el1fzopredsuc  43574  iccpartltu  43634  iccpartgtl  43635  iccpartgt  43636  iccpartleu  43637  iccpartgel  43638  fmtno4prmfac  43783  31prm  43809  sbgoldbo  44001  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  wtgoldbnnsum4prm  44016  bgoldbnnsum3prm  44018  bgoldbtbndlem3  44021  bgoldbtbnd  44023