Theorem elun 4084

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

Syntax hints:   ↔ wb 205   ∨ wo 844   = wceq 1539   ∈ wcel 2107  Vcvv 3433   ∪ cun 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893

This theorem is referenced by:  elunnel1  4085  uneqri  4086  uncom  4088  uneq1  4091  unass  4101  ssun1  4107  elunant  4113  unss1  4114  ssequn1  4115  rexun  4125  elsymdif  4182  indi  4208  undi  4209  unineq  4212  undif3  4225  rabun2  4248  reuun2  4249  undif4  4401  ssundif  4419  dfpr2  4581  elpwunsn  4620  eltpg  4622  pwpr  4834  pwtp  4835  uniun  4865  iinun2  5003  iunun  5023  iunxun  5024  iinuni  5028  brun  5126  pwunssOLD  5485  pwssun  5486  opthprc  5652  xpundi  5656  xpundir  5657  difxp  6072  sossfld  6094  elsuci  6336  elsucg  6337  elsuc2g  6338  funun  6487  mptun  6588  unima  6852  unpreima  6949  sucexeloni  7667  suceloniOLD  7669  ordsucun  7681  fnse  7983  suppofssd  8028  reldmtpos  8059  dftpos4  8070  tpostpos  8071  frrlem12  8122  frrlem13  8123  wfrlem14OLD  8162  wfrlem15OLD  8163  oarec  8402  brdom2  8779  unfi  8964  unxpdomlem3  9038  domunfican  9096  dfsup2  9212  wemapso2lem  9320  unwdomg  9352  unxpwdom2  9356  cantnfp1lem3  9447  rankunb  9617  djur  9686  djuunxp  9688  eldju2ndl  9691  eldju2ndr  9692  djuun  9693  iscard3  9858  kmlem2  9916  ssfin4  10075  dffin7-2  10163  fin1a2lem11  10175  fin1a2lem12  10176  cfpwsdom  10349  elgch  10387  fpwwe2lem12  10407  canthp1lem2  10418  gch2  10440  elnn0  12244  un0addcl  12275  un0mulcl  12276  elxnn0  12316  ltxr  12860  elxr  12861  xrsupexmnf  13048  xrinfmexpnf  13049  supxrun  13059  ixxun  13104  difreicc  13225  iccsplit  13226  fzsplit2  13290  elfzp1  13315  uzsplit  13337  elfzp12  13344  fzosplit  13429  fzouzsplit  13431  elfzonlteqm1  13472  elfzo0l  13486  fzosplitsni  13507  elfzr  13509  elfzlmr  13510  hashnn0pnf  14065  hashf1lem2  14179  hash2pwpr  14199  pr2pwpr  14202  ccatrn  14303  cats1un  14443  fsumsplit  15462  sumsplit  15489  fprodsplit  15685  rpnnen2lem12  15943  sumeven  16105  sumodd  16106  saddisjlem  16180  lcmfunsnlem1  16351  lcmfunsnlem2lem1  16352  lcmfunsnlem2lem2  16353  lcmfunsnlem2  16354  coprmprod  16375  coprmproddvdslem  16376  nnnn0modprm0  16516  prm23lt5  16524  vdwapun  16684  ramubcl  16728  basprssdmsets  16934  mreexmrid  17361  lubun  18242  smndex1basss  18553  smndex1mgm  18555  smndex1mndlem  18557  smndex1n0mnd  18560  symgextf1  19038  gsumzsplit  19537  gsumzunsnd  19566  gsumunsnfd  19567  dprddisj2  19651  dmdprdsplit2lem  19657  dmdprdsplit2  19658  dprdsplit  19660  cnfldfun  20618  mplcoe1  21247  mplcoe5  21250  evlslem4  21293  mdetunilem9  21778  maducoeval2  21798  madugsum  21801  clslp  22308  islpi  22309  restntr  22342  pnfnei  22380  mnfnei  22381  iunconn  22588  refun0  22675  xkoptsub  22814  ptunhmeo  22968  fbun  23000  filconn  23043  fixufil  23082  ufildr  23091  alexsubALTlem2  23208  alexsubALTlem3  23209  alexsubALTlem4  23210  tsmssplit  23312  xrtgioo  23978  reconnlem2  23999  iccpnfcnv  24116  iccpnfhmeo  24117  rrxcph  24565  rrxdstprj1  24582  mbfss  24819  mbfmax  24822  itg2splitlem  24922  itg2split  24923  iblss2  24979  itgsplit  25009  limcdif  25049  ellimc2  25050  limcmpt  25056  limcres  25059  limccnp  25064  limccnp2  25065  limcco  25066  rollelem  25162  dvivthlem1  25181  dvne0  25184  lhop  25189  degltlem1  25246  ply1rem  25337  fta1glem2  25340  plypf1  25382  plyaddlem1  25383  plymullem1  25384  plycj  25447  ofmulrt  25451  taylfval  25527  abelthlem2  25600  abelthlem3  25601  reasinsin  26055  scvxcvx  26144  ppinprm  26310  chtnprm  26312  dchrfi  26412  lgsdir2  26487  2lgslem3  26561  2lgsoddprmlem3  26571  usgrexmplef  27635  cffldtocusgr  27823  vtxdun  27857  eucrct2eupth  28618  shunssi  29739  atomli  30753  atoml2i  30754  rmoun  30851  rmounid  30852  elunsn  30867  nelun  30868  suppovss  31026  isoun  31043  fzsplit3  31124  eliccioo  31214  cycpmco2  31409  cyc3co2  31416  cycpmrn  31419  lindsun  31715  lbsdiflsp0  31716  ordtconnlem1  31883  xrge0iifcnv  31892  xrge0iifiso  31894  xrge0iifhom  31896  esumsplit  32030  esumpad2  32033  measvuni  32191  sxbrsigalem0  32247  bnj1138  32777  bnj1137  32984  subfacp1lem4  33154  subfacp1lem5  33155  kur14lem7  33183  satfvsucsuc  33336  satfrnmapom  33341  satf0op  33348  satf0n0  33349  sat1el2xp  33350  fmlafvel  33356  isfmlasuc  33359  fmlaomn0  33361  satfv1fvfmla1  33394  2goelgoanfmla1  33395  mrsubcv  33481  mclsax  33540  xpord2pred  33801  xpord3pred  33807  nosepdmlem  33895  ssltun1  34011  ssltun2  34012  brcup  34250  refssfne  34556  bj-eltag  35176  bj-0eltag  35177  bj-sngltag  35182  bj-projun  35193  bj-imdirco  35370  tan2h  35778  poimirlem2  35788  poimirlem8  35794  poimirlem18  35804  poimirlem21  35807  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem27  35813  poimirlem29  35815  poimirlem31  35817  poimirlem32  35818  ftc1anclem1  35859  ftc1anclem5  35863  dvasin  35870  dvacos  35871  eqfnun  35889  smprngopr  36219  elpadd  37820  paddval0  37831  hdmaplem4  39795  mapdh9a  39810  ofun  40218  lzunuz  40597  jm2.23  40825  unxpwdom3  40927  hbtlem5  40960  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  rp-fakeinunass  41129  sqrtcvallem1  41246  frege133d  41380  frege83  41561  frege131  41609  frege133  41611  uneqsn  41640  clsk1indlem3  41660  ntrneixb  41712  ntrneix3  41714  ntrneix13  41716  radcnvrat  41939  bccbc  41970  undif3VD  42509  iunconnlem2  42562  fnchoice  42579  elunnel2  42589  limciccioolb  43169  limcicciooub  43185  icccncfext  43435  cncfiooicclem1  43441  fourierdlem70  43724  fourierdlem80  43734  fourierdlem93  43747  fourierdlem101  43755  sge0split  43954  el1fzopredsuc  44828  iccpartltu  44888  iccpartgtl  44889  iccpartgt  44890  iccpartleu  44891  iccpartgel  44892  fmtno4prmfac  45035  31prm  45060  sbgoldbo  45250  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  bgoldbtbndlem3  45270  bgoldbtbnd  45272