Theorem elun 4076

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 variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3459	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3459	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3459	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 854	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2877	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
6		eleq1 2877	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶))
7	5, 6	orbi12d 916	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶)))
8		eleq1 2877	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
9		eleq1 2877	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
10	8, 9	orbi12d 916	. . 3 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
11		df-un 3886	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
12	7, 10, 11	elab2gw 3613	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
13	1, 4, 12	pm5.21nii 383	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 209   ∨ wo 844   = wceq 1538   ∈ wcel 2111  Vcvv 3441   ∪ cun 3879

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886

This theorem is referenced by:  elunnel1  4077  uneqri  4078  uncom  4080  uneq1  4083  unass  4093  ssun1  4099  elunant  4105  unss1  4106  ssequn1  4107  rexun  4117  elsymdif  4174  indi  4200  undi  4201  unineq  4204  undif3  4215  rabun2  4234  reuun2  4238  undif4  4374  ssundif  4391  dfpr2  4544  elpwunsn  4581  eltpg  4583  pwpr  4794  pwtp  4795  uniun  4823  iinun2  4958  iunun  4978  iunxun  4979  iinuni  4983  brun  5081  pwunssOLD  5420  pwssun  5421  opthprc  5580  xpundi  5584  xpundir  5585  difxp  5988  sossfld  6010  elsuci  6225  elsucg  6226  elsuc2g  6227  funun  6370  mptun  6466  unima  6714  unpreima  6810  suceloni  7508  ordsucun  7520  fnse  7810  suppofssd  7850  reldmtpos  7883  dftpos4  7894  tpostpos  7895  wfrlem14  7951  wfrlem15  7952  oarec  8171  brdom2  8522  unxpdomlem3  8708  domunfican  8775  dfsup2  8892  wemapso2lem  9000  unwdomg  9032  unxpwdom2  9036  cantnfp1lem3  9127  rankunb  9263  djur  9332  djuunxp  9334  eldju2ndl  9337  eldju2ndr  9338  djuun  9339  iscard3  9504  kmlem2  9562  ssfin4  9721  dffin7-2  9809  fin1a2lem11  9821  fin1a2lem12  9822  cfpwsdom  9995  elgch  10033  fpwwe2lem13  10053  canthp1lem2  10064  gch2  10086  elnn0  11887  un0addcl  11918  un0mulcl  11919  elxnn0  11957  ltxr  12498  elxr  12499  xrsupexmnf  12686  xrinfmexpnf  12687  supxrun  12697  ixxun  12742  difreicc  12862  iccsplit  12863  fzsplit2  12927  elfzp1  12952  uzsplit  12974  elfzp12  12981  fzosplit  13065  fzouzsplit  13067  elfzonlteqm1  13108  elfzo0l  13122  fzosplitsni  13143  elfzr  13145  elfzlmr  13146  hashnn0pnf  13698  hashf1lem2  13810  hash2pwpr  13830  pr2pwpr  13833  ccatrn  13934  cats1un  14074  fsumsplit  15089  sumsplit  15115  fprodsplit  15312  rpnnen2lem12  15570  sumeven  15728  sumodd  15729  saddisjlem  15803  lcmfunsnlem1  15971  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  lcmfunsnlem2  15974  coprmprod  15995  coprmproddvdslem  15996  nnnn0modprm0  16133  prm23lt5  16141  vdwapun  16300  ramubcl  16344  basprssdmsets  16541  mreexmrid  16906  lubun  17725  smndex1basss  18062  smndex1mgm  18064  smndex1mndlem  18066  smndex1n0mnd  18069  symgextf1  18541  gsumzsplit  19040  gsumzunsnd  19069  gsumunsnfd  19070  dprddisj2  19154  dmdprdsplit2lem  19160  dmdprdsplit2  19161  dprdsplit  19163  cnfldfunALT  20104  mplcoe1  20705  mplcoe5  20708  evlslem4  20747  mdetunilem9  21225  maducoeval2  21245  madugsum  21248  clslp  21753  islpi  21754  restntr  21787  pnfnei  21825  mnfnei  21826  iunconn  22033  refun0  22120  xkoptsub  22259  ptunhmeo  22413  fbun  22445  filconn  22488  fixufil  22527  ufildr  22536  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALTlem4  22655  tsmssplit  22757  xrtgioo  23411  reconnlem2  23432  iccpnfcnv  23549  iccpnfhmeo  23550  rrxcph  23996  rrxdstprj1  24013  mbfss  24250  mbfmax  24253  itg2splitlem  24352  itg2split  24353  iblss2  24409  itgsplit  24439  limcdif  24479  ellimc2  24480  limcmpt  24486  limcres  24489  limccnp  24494  limccnp2  24495  limcco  24496  rollelem  24592  dvivthlem1  24611  dvne0  24614  lhop  24619  degltlem1  24673  ply1rem  24764  fta1glem2  24767  plypf1  24809  plyaddlem1  24810  plymullem1  24811  plycj  24874  ofmulrt  24878  taylfval  24954  abelthlem2  25027  abelthlem3  25028  reasinsin  25482  scvxcvx  25571  ppinprm  25737  chtnprm  25739  dchrfi  25839  lgsdir2  25914  2lgslem3  25988  2lgsoddprmlem3  25998  usgrexmplef  27049  cffldtocusgr  27237  vtxdun  27271  eucrct2eupth  28030  shunssi  29151  atomli  30165  atoml2i  30166  rmoun  30265  rmounid  30266  elunsn  30281  nelun  30282  suppovss  30443  isoun  30461  fzsplit3  30543  eliccioo  30633  cycpmco2  30825  cyc3co2  30832  cycpmrn  30835  lindsun  31109  lbsdiflsp0  31110  ordtconnlem1  31277  xrge0iifcnv  31286  xrge0iifiso  31288  xrge0iifhom  31290  esumsplit  31422  esumpad2  31425  measvuni  31583  sxbrsigalem0  31639  bnj1138  32170  bnj1137  32377  subfacp1lem4  32543  subfacp1lem5  32544  kur14lem7  32572  satfvsucsuc  32725  satfrnmapom  32730  satf0op  32737  satf0n0  32738  sat1el2xp  32739  fmlafvel  32745  isfmlasuc  32748  fmlaomn0  32750  satfv1fvfmla1  32783  2goelgoanfmla1  32784  mrsubcv  32870  mclsax  32929  dftrpred3g  33185  frrlem12  33247  frrlem13  33248  nosepdmlem  33300  brcup  33513  refssfne  33819  bj-eltag  34413  bj-0eltag  34414  bj-sngltag  34419  bj-projun  34430  bj-imdirco  34605  tan2h  35049  poimirlem2  35059  poimirlem8  35065  poimirlem18  35075  poimirlem21  35078  poimirlem22  35079  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem27  35084  poimirlem29  35086  poimirlem31  35088  poimirlem32  35089  ftc1anclem1  35130  ftc1anclem5  35134  dvasin  35141  dvacos  35142  eqfnun  35160  smprngopr  35490  elpadd  37095  paddval0  37106  hdmaplem4  39070  mapdh9a  39085  ofun  39416  lzunuz  39709  jm2.23  39937  unxpwdom3  40039  hbtlem5  40072  rp-fakeinunass  40223  sqrtcvallem1  40331  frege133d  40466  frege83  40647  frege131  40695  frege133  40697  uneqsn  40726  clsk1indlem3  40746  ntrneixb  40798  ntrneix3  40800  ntrneix13  40802  radcnvrat  41018  bccbc  41049  undif3VD  41588  iunconnlem2  41641  fnchoice  41658  elunnel2  41668  limciccioolb  42263  limcicciooub  42279  icccncfext  42529  cncfiooicclem1  42535  fourierdlem70  42818  fourierdlem80  42828  fourierdlem93  42841  fourierdlem101  42849  sge0split  43048  el1fzopredsuc  43882  iccpartltu  43942  iccpartgtl  43943  iccpartgt  43944  iccpartleu  43945  iccpartgel  43946  fmtno4prmfac  44089  31prm  44114  sbgoldbo  44305  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  bgoldbtbndlem3  44325  bgoldbtbnd  44327