Theorem elun 4106

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 3459	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3459	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3459	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 857	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2816	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2816	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 918	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3910	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3638	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1540   ∈ wcel 2109  Vcvv 3438   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910

This theorem is referenced by:  elunnel1  4107  elunnel2  4108  uneqri  4109  uncom  4111  uneq1  4114  nfun  4123  unass  4125  ssun1  4131  elunant  4137  unss1  4138  ssequn1  4139  rexun  4149  elsymdif  4211  indi  4237  undi  4238  unineq  4241  undif3  4253  rabun2  4277  reuun2  4278  undif4  4420  ssundif  4441  dfpr2  4600  elunsn  4637  elpwunsn  4638  eltpg  4640  el7g  4644  pwpr  4855  pwtp  4856  uniun  4884  iinun2  5025  iunun  5045  iunxun  5046  iinuni  5050  brun  5146  pwssun  5515  opthprc  5687  xpundi  5692  xpundir  5693  imadifssran  6104  difxp  6117  sossfld  6139  elsuci  6380  elsucg  6381  elsuc2g  6382  funun  6532  mptun  6632  unima  6902  eqfnun  6975  unpreima  7001  sucexeloniOLD  7750  ordsucun  7764  resf1extb  7874  fnse  8073  xpord2pred  8085  xpord3pred  8092  suppofssd  8143  reldmtpos  8174  dftpos4  8185  tpostpos  8186  frrlem12  8237  frrlem13  8238  oarec  8487  brdom2  8914  unfi  9095  unxpdomlem3  9157  domunfican  9230  dfsup2  9353  wemapso2lem  9463  unwdomg  9495  unxpwdom2  9499  cantnfp1lem3  9595  rankunb  9765  djur  9834  djuunxp  9836  eldju2ndl  9839  eldju2ndr  9840  djuun  9841  iscard3  10006  kmlem2  10065  ssfin4  10223  dffin7-2  10311  fin1a2lem11  10323  fin1a2lem12  10324  cfpwsdom  10497  elgch  10535  fpwwe2lem12  10555  canthp1lem2  10566  gch2  10588  elnn0  12404  un0addcl  12435  un0mulcl  12436  elxnn0  12477  ltxr  13035  elxr  13036  xrsupexmnf  13225  xrinfmexpnf  13226  supxrun  13236  ixxun  13282  difreicc  13405  iccsplit  13406  fzsplit2  13470  elfzp1  13495  uzsplit  13517  elfzp12  13524  fzosplit  13613  fzouzsplit  13615  elfzonlteqm1  13662  elfzo0l  13677  fzosplitsni  13699  elfzr  13701  elfzlmr  13702  hashnn0pnf  14267  hashf1lem2  14381  hash2pwpr  14401  pr2pwpr  14404  ccatrn  14514  cats1un  14645  fsumsplit  15666  sumsplit  15693  fprodsplit  15891  rpnnen2lem12  16152  sumeven  16316  sumodd  16317  saddisjlem  16393  lcmfunsnlem1  16566  lcmfunsnlem2lem1  16567  lcmfunsnlem2lem2  16568  lcmfunsnlem2  16569  coprmprod  16590  coprmproddvdslem  16591  nnnn0modprm0  16736  prm23lt5  16744  vdwapun  16904  ramubcl  16948  basprssdmsets  17150  mreexmrid  17567  lubun  18439  smndex1basss  18797  smndex1mgm  18799  smndex1mndlem  18801  smndex1n0mnd  18804  symgextf1  19318  gsumzsplit  19824  gsumzunsnd  19853  gsumunsnfd  19854  dprddisj2  19938  dmdprdsplit2lem  19944  dmdprdsplit2  19945  dprdsplit  19947  cnfldfun  21293  cnfldfunOLD  21306  mplcoe1  21960  mplcoe5  21963  evlslem4  21999  mdetunilem9  22523  maducoeval2  22543  madugsum  22546  clslp  23051  islpi  23052  restntr  23085  pnfnei  23123  mnfnei  23124  iunconn  23331  refun0  23418  xkoptsub  23557  ptunhmeo  23711  fbun  23743  filconn  23786  fixufil  23825  ufildr  23834  alexsubALTlem2  23951  alexsubALTlem3  23952  alexsubALTlem4  23953  tsmssplit  24055  xrtgioo  24711  reconnlem2  24732  iccpnfcnv  24858  iccpnfhmeo  24859  rrxcph  25308  rrxdstprj1  25325  mbfss  25563  mbfmax  25566  itg2splitlem  25665  itg2split  25666  iblss2  25723  itgsplit  25753  limcdif  25793  ellimc2  25794  limcmpt  25800  limcres  25803  limccnp  25808  limccnp2  25809  limcco  25810  rollelem  25909  dvivthlem1  25929  dvne0  25932  lhop  25937  degltlem1  25993  ply1rem  26087  fta1glem2  26090  plypf1  26133  plyaddlem1  26134  plymullem1  26135  plycj  26199  plycjOLD  26201  ofmulrt  26205  taylfval  26282  abelthlem2  26358  abelthlem3  26359  reasinsin  26822  scvxcvx  26912  ppinprm  27078  chtnprm  27080  dchrfi  27182  lgsdir2  27257  2lgslem3  27331  2lgsoddprmlem3  27341  nosepdmlem  27611  ssltun1  27737  ssltun2  27738  addsproplem2  27900  addsuniflem  27931  negsid  27970  mulsproplem9  28050  ssltmul1  28073  ssltmul2  28074  precsexlem9  28140  precsexlem11  28142  sltonold  28185  usgrexmplef  29222  cffldtocusgr  29410  cffldtocusgrOLD  29411  vtxdun  29445  eucrct2eupth  30207  shunssi  31330  atomli  32344  atoml2i  32345  rmoun  32456  rmounid  32457  nelun  32475  suppovss  32637  isoun  32658  fzsplit3  32749  eliccioo  32884  chnccats1  32970  gsumwun  33031  cycpmco2  33088  cyc3co2  33095  cycpmrn  33098  elrgspnlem2  33193  ply1dg3rt0irred  33527  lindsun  33597  lbsdiflsp0  33598  ordtconnlem1  33890  xrge0iifcnv  33899  xrge0iifiso  33901  xrge0iifhom  33903  esumsplit  34019  esumpad2  34022  measvuni  34180  sxbrsigalem0  34238  bnj1138  34754  bnj1137  34961  subfacp1lem4  35155  subfacp1lem5  35156  kur14lem7  35184  satfvsucsuc  35337  satfrnmapom  35342  satf0op  35349  satf0n0  35350  sat1el2xp  35351  fmlafvel  35357  isfmlasuc  35360  fmlaomn0  35362  satfv1fvfmla1  35395  2goelgoanfmla1  35396  mrsubcv  35482  mclsax  35541  brcup  35912  refssfne  36331  bj-eltag  36950  bj-0eltag  36951  bj-sngltag  36956  bj-projun  36967  bj-axbun  37009  bj-axadj  37014  bj-imdirco  37163  tan2h  37591  poimirlem2  37601  poimirlem8  37607  poimirlem18  37617  poimirlem21  37620  poimirlem22  37621  poimirlem23  37622  poimirlem24  37623  poimirlem25  37624  poimirlem27  37626  poimirlem29  37628  poimirlem31  37630  poimirlem32  37631  ftc1anclem1  37672  ftc1anclem5  37676  dvasin  37683  dvacos  37684  smprngopr  38031  elpadd  39778  paddval0  39789  hdmaplem4  41753  mapdh9a  41768  unitscyglem2  42169  ofun  42209  lzunuz  42741  jm2.23  42969  unxpwdom3  43068  hbtlem5  43101  fzunt  43428  fzuntd  43429  fzunt1d  43430  fzuntgd  43431  rp-fakeinunass  43488  sqrtcvallem1  43604  frege133d  43738  frege83  43919  frege131  43967  frege133  43969  uneqsn  43998  clsk1indlem3  44016  ntrneixb  44068  ntrneix3  44070  ntrneix13  44072  radcnvrat  44287  bccbc  44318  undif3VD  44855  iunconnlem2  44908  permaxinf2lem  44986  fnchoice  45007  limciccioolb  45603  limcicciooub  45619  icccncfext  45869  cncfiooicclem1  45875  fourierdlem70  46158  fourierdlem80  46168  fourierdlem93  46181  fourierdlem101  46189  sge0split  46391  el1fzopredsuc  47310  iccpartltu  47410  iccpartgtl  47411  iccpartgt  47412  iccpartleu  47413  iccpartgel  47414  fmtno4prmfac  47557  31prm  47582  sbgoldbo  47772  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  wtgoldbnnsum4prm  47787  bgoldbnnsum3prm  47789  bgoldbtbndlem3  47792  bgoldbtbnd  47794  elclnbgrelnbgr  47810  clnbgrel  47813  clnbupgrel  47819  dfclnbgr6  47841  isubgr3stgrlem4  47954  usgrexmpl1tri  48010  usgrexmpl2nb0  48016  usgrexmpl2nb1  48017  usgrexmpl2nb2  48018  usgrexmpl2nb3  48019  usgrexmpl2nb4  48020  usgrexmpl2nb5  48021  usgrexmpl2trifr  48022  gpgprismgr4cycllem3  48082  gpgprismgr4cycllem7  48086  gpgprismgr4cycllem10  48089