Theorem elun 4090

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 3453	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3453	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3453	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 863	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2828	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2828	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 924	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3895	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3625	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 379	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 207   ∨ wo 853   = wceq 1547   ∈ wcel 2119  Vcvv 3432   ∪ cun 3888

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895

This theorem is referenced by:  elunnel1  4091  elunnel2  4092  uneqri  4093  uncom  4095  uneq1  4098  nfun  4107  unass  4108  ssun1  4114  elunant  4120  unss1  4121  ssequn1  4122  rexun  4132  elsymdif  4193  indi  4219  undi  4220  unineq  4223  undif3  4235  rabun2  4259  reuun2  4260  undif4  4402  ssundif  4422  dfpr2  4583  elunsn  4622  elpwunsn  4623  eltpg  4625  el7g  4629  pwpr  4839  pwtp  4840  uniun  4868  iinun2  5009  iunun  5029  iunxun  5030  iinuni  5034  brun  5130  trun  5197  pwssun  5517  opthprc  5689  xpundi  5694  xpundir  5695  imadifssran  6109  difxp  6122  sossfld  6144  elsuci  6386  elsucg  6387  elsuc2g  6388  funun  6538  mptun  6638  unima  6909  eqfnun  6985  unpreima  7011  ordsucun  7772  resf1extb  7881  fnse  8080  xpord2pred  8092  xpord3pred  8099  suppofssd  8150  reldmtpos  8181  dftpos4  8192  tpostpos  8193  frrlem12  8244  frrlem13  8245  oarec  8494  brdom2  8926  unfi  9102  unxpdomlem3  9165  domunfican  9229  dfsup2  9354  wemapso2lem  9464  unwdomg  9496  unxpwdom2  9500  cantnfp1lem3  9599  rankunb  9772  djur  9841  djuunxp  9843  eldju2ndl  9846  eldju2ndr  9847  djuun  9848  iscard3  10013  kmlem2  10072  ssfin4  10230  dffin7-2  10318  fin1a2lem11  10330  fin1a2lem12  10331  cfpwsdom  10505  elgch  10543  fpwwe2lem12  10563  canthp1lem2  10574  gch2  10596  elnn0  12437  un0addcl  12468  un0mulcl  12469  elxnn0  12510  ltxr  13064  elxr  13065  xrsupexmnf  13255  xrinfmexpnf  13256  supxrun  13266  ixxun  13312  difreicc  13435  iccsplit  13436  fzsplit2  13501  elfzp1  13526  uzsplit  13548  elfzp12  13555  fzosplit  13645  fzouzsplit  13647  elfzonlteqm1  13694  elfzo0l  13709  fzosplitsni  13732  elfzr  13734  elfzlmr  13735  hashnn0pnf  14302  hashf1lem2  14416  hash2pwpr  14436  pr2pwpr  14439  ccatrn  14550  cats1un  14681  fsumsplit  15701  sumsplit  15728  fprodsplit  15929  rpnnen2lem12  16190  sumeven  16354  sumodd  16355  saddisjlem  16431  lcmfunsnlem1  16604  lcmfunsnlem2lem1  16605  lcmfunsnlem2lem2  16606  lcmfunsnlem2  16607  coprmprod  16628  coprmproddvdslem  16629  nnnn0modprm0  16775  prm23lt5  16783  vdwapun  16943  ramubcl  16987  basprssdmsets  17189  mreexmrid  17607  lubun  18479  chnccats1  18589  smndex1basss  18874  smndex1mgm  18876  smndex1mndlem  18878  smndex1n0mnd  18881  symgextf1  19394  gsumzsplit  19900  gsumzunsnd  19929  gsumunsnfd  19930  dprddisj2  20014  dmdprdsplit2lem  20020  dmdprdsplit2  20021  dprdsplit  20023  cnfldfun  21368  mplcoe1  22020  mplcoe5  22023  evlslem4  22059  mdetunilem9  22610  maducoeval2  22630  madugsum  22633  clslp  23138  islpi  23139  restntr  23172  pnfnei  23210  mnfnei  23211  iunconn  23418  refun0  23505  xkoptsub  23644  ptunhmeo  23798  fbun  23830  filconn  23873  fixufil  23912  ufildr  23921  alexsubALTlem2  24038  alexsubALTlem3  24039  alexsubALTlem4  24040  tsmssplit  24142  xrtgioo  24797  reconnlem2  24818  iccpnfcnv  24936  iccpnfhmeo  24937  rrxcph  25384  rrxdstprj1  25401  mbfss  25638  mbfmax  25641  itg2splitlem  25740  itg2split  25741  iblss2  25798  itgsplit  25828  limcdif  25868  ellimc2  25869  limcmpt  25875  limcres  25878  limccnp  25883  limccnp2  25884  limcco  25885  rollelem  25981  dvivthlem1  26000  dvne0  26003  lhop  26008  degltlem1  26062  ply1rem  26156  fta1glem2  26159  plypf1  26202  plyaddlem1  26203  plymullem1  26204  plycj  26267  plycjOLD  26269  ofmulrt  26273  taylfval  26349  abelthlem2  26422  abelthlem3  26423  reasinsin  26885  scvxcvx  26974  ppinprm  27140  chtnprm  27142  dchrfi  27243  lgsdir2  27318  2lgslem3  27392  2lgsoddprmlem3  27402  nosepdmlem  27672  sltsun1  27805  sltsun2  27806  addsproplem2  27987  addsuniflem  28018  negsid  28058  mulsproplem9  28141  sltmuls1  28164  sltmuls2  28165  precsexlem9  28232  precsexlem11  28234  ltonold  28278  usgrexmplef  29353  cffldtocusgr  29541  vtxdun  29575  eucrct2eupth  30340  shunssi  31464  atomli  32478  atoml2i  32479  rmoun  32588  rmounid  32589  nelun  32608  suppovss  32780  isoun  32801  fzsplit3  32892  eliccioo  33016  gsumwun  33164  cycpmco2  33221  cyc3co2  33228  cycpmrn  33231  elrgspnlem2  33331  ply1dg3rt0irred  33674  lindsun  33816  lbsdiflsp0  33817  ordtconnlem1  34115  xrge0iifcnv  34124  xrge0iifiso  34126  xrge0iifhom  34128  esumsplit  34244  esumpad2  34247  measvuni  34405  sxbrsigalem0  34462  bnj1138  34978  bnj1137  35184  subfacp1lem4  35418  subfacp1lem5  35419  kur14lem7  35447  satfvsucsuc  35600  satfrnmapom  35605  satf0op  35612  satf0n0  35613  sat1el2xp  35614  fmlafvel  35620  isfmlasuc  35623  fmlaomn0  35625  satfv1fvfmla1  35658  2goelgoanfmla1  35659  mrsubcv  35745  mclsax  35804  brcup  36172  refssfne  36593  ttciunun  36746  bj-eltag  37337  bj-0eltag  37338  bj-sngltag  37343  bj-projun  37354  bj-axbun  37396  bj-axadj  37401  bj-imdirco  37557  tan2h  37986  poimirlem2  37996  poimirlem8  38002  poimirlem18  38012  poimirlem21  38015  poimirlem22  38016  poimirlem23  38017  poimirlem24  38018  poimirlem25  38019  poimirlem27  38021  poimirlem29  38023  poimirlem31  38025  poimirlem32  38026  ftc1anclem1  38067  ftc1anclem5  38071  dvasin  38078  dvacos  38079  smprngopr  38426  dfsucmap3  38837  elpadd  40298  paddval0  40309  hdmaplem4  42273  mapdh9a  42288  unitscyglem2  42688  ofun  42729  lzunuz  43224  jm2.23  43448  unxpwdom3  43547  hbtlem5  43580  fzunt  43906  fzuntd  43907  fzunt1d  43908  fzuntgd  43909  rp-fakeinunass  43966  sqrtcvallem1  44082  frege133d  44216  frege83  44397  frege131  44445  frege133  44447  uneqsn  44476  clsk1indlem3  44494  ntrneixb  44546  ntrneix3  44548  ntrneix13  44550  radcnvrat  44765  bccbc  44796  undif3VD  45332  iunconnlem2  45385  permaxinf2lem  45463  fnchoice  45484  limciccioolb  46073  limcicciooub  46087  icccncfext  46337  cncfiooicclem1  46343  fourierdlem70  46626  fourierdlem80  46636  fourierdlem93  46649  fourierdlem101  46657  sge0split  46859  el1fzopredsuc  47796  iccpartltu  47907  iccpartgtl  47908  iccpartgt  47909  iccpartleu  47910  iccpartgel  47911  fmtno4prmfac  48057  31prm  48082  sbgoldbo  48285  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  wtgoldbnnsum4prm  48300  bgoldbnnsum3prm  48302  bgoldbtbndlem3  48305  bgoldbtbnd  48307  elclnbgrelnbgr  48323  clnbgrel  48326  clnbupgrel  48332  dfclnbgr6  48354  isubgr3stgrlem4  48467  usgrexmpl1tri  48523  usgrexmpl2nb0  48529  usgrexmpl2nb1  48530  usgrexmpl2nb2  48531  usgrexmpl2nb3  48532  usgrexmpl2nb4  48533  usgrexmpl2nb5  48534  usgrexmpl2trifr  48535  gpgprismgr4cycllem3  48595  gpgprismgr4cycllem7  48599  gpgprismgr4cycllem10  48602