Theorem elun 4088

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 3449	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3449	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3449	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 854	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2828	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2828	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 916	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3897	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3613	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 380	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 205   ∨ wo 844   = wceq 1542   ∈ wcel 2110  Vcvv 3431   ∪ cun 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-un 3897

This theorem is referenced by:  elunnel1  4089  uneqri  4090  uncom  4092  uneq1  4095  unass  4105  ssun1  4111  elunant  4117  unss1  4118  ssequn1  4119  rexun  4129  elsymdif  4187  indi  4213  undi  4214  unineq  4217  undif3  4230  rabun2  4253  reuun2  4254  undif4  4406  ssundif  4424  dfpr2  4586  elpwunsn  4625  eltpg  4627  pwpr  4839  pwtp  4840  uniun  4870  iinun2  5007  iunun  5027  iunxun  5028  iinuni  5032  brun  5130  pwunssOLD  5484  pwssun  5485  opthprc  5651  xpundi  5655  xpundir  5656  difxp  6065  sossfld  6087  elsuci  6330  elsucg  6331  elsuc2g  6332  funun  6477  mptun  6576  unima  6838  unpreima  6935  suceloni  7649  ordsucun  7661  fnse  7959  suppofssd  8004  reldmtpos  8035  dftpos4  8046  tpostpos  8047  frrlem12  8098  frrlem13  8099  wfrlem14OLD  8138  wfrlem15OLD  8139  oarec  8370  brdom2  8745  unfi  8929  unxpdomlem3  8999  domunfican  9057  dfsup2  9173  wemapso2lem  9281  unwdomg  9313  unxpwdom2  9317  cantnfp1lem3  9408  dftrpred3g  9473  rankunb  9601  djur  9670  djuunxp  9672  eldju2ndl  9675  eldju2ndr  9676  djuun  9677  iscard3  9842  kmlem2  9900  ssfin4  10059  dffin7-2  10147  fin1a2lem11  10159  fin1a2lem12  10160  cfpwsdom  10333  elgch  10371  fpwwe2lem12  10391  canthp1lem2  10402  gch2  10424  elnn0  12227  un0addcl  12258  un0mulcl  12259  elxnn0  12299  ltxr  12842  elxr  12843  xrsupexmnf  13030  xrinfmexpnf  13031  supxrun  13041  ixxun  13086  difreicc  13207  iccsplit  13208  fzsplit2  13272  elfzp1  13297  uzsplit  13319  elfzp12  13326  fzosplit  13410  fzouzsplit  13412  elfzonlteqm1  13453  elfzo0l  13467  fzosplitsni  13488  elfzr  13490  elfzlmr  13491  hashnn0pnf  14046  hashf1lem2  14160  hash2pwpr  14180  pr2pwpr  14183  ccatrn  14284  cats1un  14424  fsumsplit  15443  sumsplit  15470  fprodsplit  15666  rpnnen2lem12  15924  sumeven  16086  sumodd  16087  saddisjlem  16161  lcmfunsnlem1  16332  lcmfunsnlem2lem1  16333  lcmfunsnlem2lem2  16334  lcmfunsnlem2  16335  coprmprod  16356  coprmproddvdslem  16357  nnnn0modprm0  16497  prm23lt5  16505  vdwapun  16665  ramubcl  16709  basprssdmsets  16915  mreexmrid  17342  lubun  18223  smndex1basss  18534  smndex1mgm  18536  smndex1mndlem  18538  smndex1n0mnd  18541  symgextf1  19019  gsumzsplit  19518  gsumzunsnd  19547  gsumunsnfd  19548  dprddisj2  19632  dmdprdsplit2lem  19638  dmdprdsplit2  19639  dprdsplit  19641  cnfldfunALT  20601  mplcoe1  21228  mplcoe5  21231  evlslem4  21274  mdetunilem9  21759  maducoeval2  21779  madugsum  21782  clslp  22289  islpi  22290  restntr  22323  pnfnei  22361  mnfnei  22362  iunconn  22569  refun0  22656  xkoptsub  22795  ptunhmeo  22949  fbun  22981  filconn  23024  fixufil  23063  ufildr  23072  alexsubALTlem2  23189  alexsubALTlem3  23190  alexsubALTlem4  23191  tsmssplit  23293  xrtgioo  23959  reconnlem2  23980  iccpnfcnv  24097  iccpnfhmeo  24098  rrxcph  24546  rrxdstprj1  24563  mbfss  24800  mbfmax  24803  itg2splitlem  24903  itg2split  24904  iblss2  24960  itgsplit  24990  limcdif  25030  ellimc2  25031  limcmpt  25037  limcres  25040  limccnp  25045  limccnp2  25046  limcco  25047  rollelem  25143  dvivthlem1  25162  dvne0  25165  lhop  25170  degltlem1  25227  ply1rem  25318  fta1glem2  25321  plypf1  25363  plyaddlem1  25364  plymullem1  25365  plycj  25428  ofmulrt  25432  taylfval  25508  abelthlem2  25581  abelthlem3  25582  reasinsin  26036  scvxcvx  26125  ppinprm  26291  chtnprm  26293  dchrfi  26393  lgsdir2  26468  2lgslem3  26542  2lgsoddprmlem3  26552  usgrexmplef  27616  cffldtocusgr  27804  vtxdun  27838  eucrct2eupth  28597  shunssi  29718  atomli  30732  atoml2i  30733  rmoun  30830  rmounid  30831  elunsn  30846  nelun  30847  suppovss  31005  isoun  31022  fzsplit3  31103  eliccioo  31193  cycpmco2  31388  cyc3co2  31395  cycpmrn  31398  lindsun  31694  lbsdiflsp0  31695  ordtconnlem1  31862  xrge0iifcnv  31871  xrge0iifiso  31873  xrge0iifhom  31875  esumsplit  32009  esumpad2  32012  measvuni  32170  sxbrsigalem0  32226  bnj1138  32756  bnj1137  32963  subfacp1lem4  33133  subfacp1lem5  33134  kur14lem7  33162  satfvsucsuc  33315  satfrnmapom  33320  satf0op  33327  satf0n0  33328  sat1el2xp  33329  fmlafvel  33335  isfmlasuc  33338  fmlaomn0  33340  satfv1fvfmla1  33373  2goelgoanfmla1  33374  mrsubcv  33460  mclsax  33519  xpord2pred  33780  xpord3pred  33786  nosepdmlem  33874  ssltun1  33990  ssltun2  33991  brcup  34229  refssfne  34535  bj-eltag  35155  bj-0eltag  35156  bj-sngltag  35161  bj-projun  35172  bj-imdirco  35349  tan2h  35757  poimirlem2  35767  poimirlem8  35773  poimirlem18  35783  poimirlem21  35786  poimirlem22  35787  poimirlem23  35788  poimirlem24  35789  poimirlem25  35790  poimirlem27  35792  poimirlem29  35794  poimirlem31  35796  poimirlem32  35797  ftc1anclem1  35838  ftc1anclem5  35842  dvasin  35849  dvacos  35850  eqfnun  35868  smprngopr  36198  elpadd  37801  paddval0  37812  hdmaplem4  39776  mapdh9a  39791  ofun  40200  lzunuz  40579  jm2.23  40807  unxpwdom3  40909  hbtlem5  40942  rp-fakeinunass  41093  sqrtcvallem1  41201  frege133d  41335  frege83  41516  frege131  41564  frege133  41566  uneqsn  41595  clsk1indlem3  41615  ntrneixb  41667  ntrneix3  41669  ntrneix13  41671  radcnvrat  41894  bccbc  41925  undif3VD  42464  iunconnlem2  42517  fnchoice  42534  elunnel2  42544  limciccioolb  43125  limcicciooub  43141  icccncfext  43391  cncfiooicclem1  43397  fourierdlem70  43680  fourierdlem80  43690  fourierdlem93  43703  fourierdlem101  43711  sge0split  43910  el1fzopredsuc  44778  iccpartltu  44838  iccpartgtl  44839  iccpartgt  44840  iccpartleu  44841  iccpartgel  44842  fmtno4prmfac  44985  31prm  45010  sbgoldbo  45200  nnsum4primeseven  45213  nnsum4primesevenALTV  45214  wtgoldbnnsum4prm  45215  bgoldbnnsum3prm  45217  bgoldbtbndlem3  45220  bgoldbtbnd  45222