Theorem elun 4148

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

Syntax hints:   ↔ wb 205   ∨ wo 844   = wceq 1540   ∈ wcel 2105  Vcvv 3473   ∪ cun 3946

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3953

This theorem is referenced by:  elunnel1  4149  elunnel2  4150  uneqri  4151  uncom  4153  uneq1  4156  unass  4166  ssun1  4172  elunant  4178  unss1  4179  ssequn1  4180  rexun  4190  elsymdif  4247  indi  4273  undi  4274  unineq  4277  undif3  4290  rabun2  4313  reuun2  4314  undif4  4466  ssundif  4487  dfpr2  4647  elpwunsn  4687  eltpg  4689  pwpr  4902  pwtp  4903  uniun  4934  iinun2  5076  iunun  5096  iunxun  5097  iinuni  5101  brun  5199  pwssun  5571  opthprc  5740  xpundi  5744  xpundir  5745  difxp  6163  sossfld  6185  elsuci  6431  elsucg  6432  elsuc2g  6433  funun  6594  mptun  6696  unima  6966  eqfnun  7038  unpreima  7064  sucexeloniOLD  7802  suceloniOLD  7804  ordsucun  7817  fnse  8124  xpord2pred  8136  xpord3pred  8143  suppofssd  8194  reldmtpos  8225  dftpos4  8236  tpostpos  8237  frrlem12  8288  frrlem13  8289  wfrlem14OLD  8328  wfrlem15OLD  8329  oarec  8568  brdom2  8984  unfi  9178  unxpdomlem3  9258  domunfican  9326  dfsup2  9445  wemapso2lem  9553  unwdomg  9585  unxpwdom2  9589  cantnfp1lem3  9681  rankunb  9851  djur  9920  djuunxp  9922  eldju2ndl  9925  eldju2ndr  9926  djuun  9927  iscard3  10094  kmlem2  10152  ssfin4  10311  dffin7-2  10399  fin1a2lem11  10411  fin1a2lem12  10412  cfpwsdom  10585  elgch  10623  fpwwe2lem12  10643  canthp1lem2  10654  gch2  10676  elnn0  12481  un0addcl  12512  un0mulcl  12513  elxnn0  12553  ltxr  13102  elxr  13103  xrsupexmnf  13291  xrinfmexpnf  13292  supxrun  13302  ixxun  13347  difreicc  13468  iccsplit  13469  fzsplit2  13533  elfzp1  13558  uzsplit  13580  elfzp12  13587  fzosplit  13672  fzouzsplit  13674  elfzonlteqm1  13715  elfzo0l  13729  fzosplitsni  13750  elfzr  13752  elfzlmr  13753  hashnn0pnf  14309  hashf1lem2  14424  hash2pwpr  14444  pr2pwpr  14447  ccatrn  14546  cats1un  14678  fsumsplit  15694  sumsplit  15721  fprodsplit  15917  rpnnen2lem12  16175  sumeven  16337  sumodd  16338  saddisjlem  16412  lcmfunsnlem1  16581  lcmfunsnlem2lem1  16582  lcmfunsnlem2lem2  16583  lcmfunsnlem2  16584  coprmprod  16605  coprmproddvdslem  16606  nnnn0modprm0  16746  prm23lt5  16754  vdwapun  16914  ramubcl  16958  basprssdmsets  17164  mreexmrid  17594  lubun  18475  smndex1basss  18825  smndex1mgm  18827  smndex1mndlem  18829  smndex1n0mnd  18832  symgextf1  19334  gsumzsplit  19840  gsumzunsnd  19869  gsumunsnfd  19870  dprddisj2  19954  dmdprdsplit2lem  19960  dmdprdsplit2  19961  dprdsplit  19963  cnfldfun  21160  mplcoe1  21816  mplcoe5  21819  evlslem4  21861  mdetunilem9  22355  maducoeval2  22375  madugsum  22378  clslp  22885  islpi  22886  restntr  22919  pnfnei  22957  mnfnei  22958  iunconn  23165  refun0  23252  xkoptsub  23391  ptunhmeo  23545  fbun  23577  filconn  23620  fixufil  23659  ufildr  23668  alexsubALTlem2  23785  alexsubALTlem3  23786  alexsubALTlem4  23787  tsmssplit  23889  xrtgioo  24555  reconnlem2  24576  iccpnfcnv  24702  iccpnfhmeo  24703  rrxcph  25153  rrxdstprj1  25170  mbfss  25408  mbfmax  25411  itg2splitlem  25511  itg2split  25512  iblss2  25568  itgsplit  25598  limcdif  25638  ellimc2  25639  limcmpt  25645  limcres  25648  limccnp  25653  limccnp2  25654  limcco  25655  rollelem  25754  dvivthlem1  25774  dvne0  25777  lhop  25782  degltlem1  25839  ply1rem  25930  fta1glem2  25933  plypf1  25975  plyaddlem1  25976  plymullem1  25977  plycj  26041  ofmulrt  26045  taylfval  26121  abelthlem2  26195  abelthlem3  26196  reasinsin  26652  scvxcvx  26741  ppinprm  26907  chtnprm  26909  dchrfi  27009  lgsdir2  27084  2lgslem3  27158  2lgsoddprmlem3  27168  nosepdmlem  27437  ssltun1  27561  ssltun2  27562  addsproplem2  27707  addsuniflem  27738  negsid  27769  mulsproplem9  27834  ssltmul1  27856  ssltmul2  27857  precsexlem9  27915  precsexlem11  27917  sltonold  27941  usgrexmplef  28798  cffldtocusgr  28986  vtxdun  29020  eucrct2eupth  29780  shunssi  30903  atomli  31917  atoml2i  31918  rmoun  32016  rmounid  32017  elunsn  32032  nelun  32033  suppovss  32188  isoun  32205  fzsplit3  32287  eliccioo  32379  cycpmco2  32577  cyc3co2  32584  cycpmrn  32587  lindsun  33013  lbsdiflsp0  33014  ordtconnlem1  33217  xrge0iifcnv  33226  xrge0iifiso  33228  xrge0iifhom  33230  esumsplit  33364  esumpad2  33367  measvuni  33525  sxbrsigalem0  33583  bnj1138  34112  bnj1137  34319  subfacp1lem4  34487  subfacp1lem5  34488  kur14lem7  34516  satfvsucsuc  34669  satfrnmapom  34674  satf0op  34681  satf0n0  34682  sat1el2xp  34683  fmlafvel  34689  isfmlasuc  34692  fmlaomn0  34694  satfv1fvfmla1  34727  2goelgoanfmla1  34728  mrsubcv  34814  mclsax  34873  brcup  35230  gg-cnfldfun  35496  gg-cffldtocusgr  35498  refssfne  35559  bj-eltag  36174  bj-0eltag  36175  bj-sngltag  36180  bj-projun  36191  bj-axbun  36233  bj-axadj  36238  bj-imdirco  36387  tan2h  36796  poimirlem2  36806  poimirlem8  36812  poimirlem18  36822  poimirlem21  36825  poimirlem22  36826  poimirlem23  36827  poimirlem24  36828  poimirlem25  36829  poimirlem27  36831  poimirlem29  36833  poimirlem31  36835  poimirlem32  36836  ftc1anclem1  36877  ftc1anclem5  36881  dvasin  36888  dvacos  36889  smprngopr  37236  elpadd  38986  paddval0  38997  hdmaplem4  40961  mapdh9a  40976  ofun  41377  lzunuz  41821  jm2.23  42050  unxpwdom3  42152  hbtlem5  42185  fzunt  42521  fzuntd  42522  fzunt1d  42523  fzuntgd  42524  rp-fakeinunass  42581  sqrtcvallem1  42697  frege133d  42831  frege83  43012  frege131  43060  frege133  43062  uneqsn  43091  clsk1indlem3  43109  ntrneixb  43161  ntrneix3  43163  ntrneix13  43165  radcnvrat  43388  bccbc  43419  undif3VD  43958  iunconnlem2  44011  fnchoice  44028  limciccioolb  44648  limcicciooub  44664  icccncfext  44914  cncfiooicclem1  44920  fourierdlem70  45203  fourierdlem80  45213  fourierdlem93  45226  fourierdlem101  45234  sge0split  45436  el1fzopredsuc  46344  iccpartltu  46404  iccpartgtl  46405  iccpartgt  46406  iccpartleu  46407  iccpartgel  46408  fmtno4prmfac  46551  31prm  46576  sbgoldbo  46766  nnsum4primeseven  46779  nnsum4primesevenALTV  46780  wtgoldbnnsum4prm  46781  bgoldbnnsum3prm  46783  bgoldbtbndlem3  46786  bgoldbtbnd  46788