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

Syntax hints:   ↔ wb 205   ∨ wo 846   = wceq 1542   ∈ wcel 2107  Vcvv 3475   ∪ cun 3946

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  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  5739  xpundi  5743  xpundir  5744  difxp  6161  sossfld  6183  elsuci  6429  elsucg  6430  elsuc2g  6431  funun  6592  mptun  6694  unima  6964  eqfnun  7036  unpreima  7062  sucexeloniOLD  7795  suceloniOLD  7797  ordsucun  7810  fnse  8116  xpord2pred  8128  xpord3pred  8135  suppofssd  8185  reldmtpos  8216  dftpos4  8227  tpostpos  8228  frrlem12  8279  frrlem13  8280  wfrlem14OLD  8319  wfrlem15OLD  8320  oarec  8559  brdom2  8975  unfi  9169  unxpdomlem3  9249  domunfican  9317  dfsup2  9436  wemapso2lem  9544  unwdomg  9576  unxpwdom2  9580  cantnfp1lem3  9672  rankunb  9842  djur  9911  djuunxp  9913  eldju2ndl  9916  eldju2ndr  9917  djuun  9918  iscard3  10085  kmlem2  10143  ssfin4  10302  dffin7-2  10390  fin1a2lem11  10402  fin1a2lem12  10403  cfpwsdom  10576  elgch  10614  fpwwe2lem12  10634  canthp1lem2  10645  gch2  10667  elnn0  12471  un0addcl  12502  un0mulcl  12503  elxnn0  12543  ltxr  13092  elxr  13093  xrsupexmnf  13281  xrinfmexpnf  13282  supxrun  13292  ixxun  13337  difreicc  13458  iccsplit  13459  fzsplit2  13523  elfzp1  13548  uzsplit  13570  elfzp12  13577  fzosplit  13662  fzouzsplit  13664  elfzonlteqm1  13705  elfzo0l  13719  fzosplitsni  13740  elfzr  13742  elfzlmr  13743  hashnn0pnf  14299  hashf1lem2  14414  hash2pwpr  14434  pr2pwpr  14437  ccatrn  14536  cats1un  14668  fsumsplit  15684  sumsplit  15711  fprodsplit  15907  rpnnen2lem12  16165  sumeven  16327  sumodd  16328  saddisjlem  16402  lcmfunsnlem1  16571  lcmfunsnlem2lem1  16572  lcmfunsnlem2lem2  16573  lcmfunsnlem2  16574  coprmprod  16595  coprmproddvdslem  16596  nnnn0modprm0  16736  prm23lt5  16744  vdwapun  16904  ramubcl  16948  basprssdmsets  17154  mreexmrid  17584  lubun  18465  smndex1basss  18783  smndex1mgm  18785  smndex1mndlem  18787  smndex1n0mnd  18790  symgextf1  19284  gsumzsplit  19790  gsumzunsnd  19819  gsumunsnfd  19820  dprddisj2  19904  dmdprdsplit2lem  19910  dmdprdsplit2  19911  dprdsplit  19913  cnfldfun  20949  mplcoe1  21584  mplcoe5  21587  evlslem4  21629  mdetunilem9  22114  maducoeval2  22134  madugsum  22137  clslp  22644  islpi  22645  restntr  22678  pnfnei  22716  mnfnei  22717  iunconn  22924  refun0  23011  xkoptsub  23150  ptunhmeo  23304  fbun  23336  filconn  23379  fixufil  23418  ufildr  23427  alexsubALTlem2  23544  alexsubALTlem3  23545  alexsubALTlem4  23546  tsmssplit  23648  xrtgioo  24314  reconnlem2  24335  iccpnfcnv  24452  iccpnfhmeo  24453  rrxcph  24901  rrxdstprj1  24918  mbfss  25155  mbfmax  25158  itg2splitlem  25258  itg2split  25259  iblss2  25315  itgsplit  25345  limcdif  25385  ellimc2  25386  limcmpt  25392  limcres  25395  limccnp  25400  limccnp2  25401  limcco  25402  rollelem  25498  dvivthlem1  25517  dvne0  25520  lhop  25525  degltlem1  25582  ply1rem  25673  fta1glem2  25676  plypf1  25718  plyaddlem1  25719  plymullem1  25720  plycj  25783  ofmulrt  25787  taylfval  25863  abelthlem2  25936  abelthlem3  25937  reasinsin  26391  scvxcvx  26480  ppinprm  26646  chtnprm  26648  dchrfi  26748  lgsdir2  26823  2lgslem3  26897  2lgsoddprmlem3  26907  nosepdmlem  27176  ssltun1  27299  ssltun2  27300  addsproplem2  27444  addsuniflem  27474  negsid  27505  mulsproplem9  27570  ssltmul1  27592  ssltmul2  27593  precsexlem9  27651  precsexlem11  27653  usgrexmplef  28506  cffldtocusgr  28694  vtxdun  28728  eucrct2eupth  29488  shunssi  30609  atomli  31623  atoml2i  31624  rmoun  31722  rmounid  31723  elunsn  31738  nelun  31739  suppovss  31894  isoun  31911  fzsplit3  31993  eliccioo  32085  cycpmco2  32280  cyc3co2  32287  cycpmrn  32290  lindsun  32699  lbsdiflsp0  32700  ordtconnlem1  32893  xrge0iifcnv  32902  xrge0iifiso  32904  xrge0iifhom  32906  esumsplit  33040  esumpad2  33043  measvuni  33201  sxbrsigalem0  33259  bnj1138  33788  bnj1137  33995  subfacp1lem4  34163  subfacp1lem5  34164  kur14lem7  34192  satfvsucsuc  34345  satfrnmapom  34350  satf0op  34357  satf0n0  34358  sat1el2xp  34359  fmlafvel  34365  isfmlasuc  34368  fmlaomn0  34370  satfv1fvfmla1  34403  2goelgoanfmla1  34404  mrsubcv  34490  mclsax  34549  brcup  34900  refssfne  35232  bj-eltag  35847  bj-0eltag  35848  bj-sngltag  35853  bj-projun  35864  bj-axbun  35906  bj-axadj  35911  bj-imdirco  36060  tan2h  36469  poimirlem2  36479  poimirlem8  36485  poimirlem18  36495  poimirlem21  36498  poimirlem22  36499  poimirlem23  36500  poimirlem24  36501  poimirlem25  36502  poimirlem27  36504  poimirlem29  36506  poimirlem31  36508  poimirlem32  36509  ftc1anclem1  36550  ftc1anclem5  36554  dvasin  36561  dvacos  36562  smprngopr  36909  elpadd  38659  paddval0  38670  hdmaplem4  40634  mapdh9a  40649  ofun  41056  lzunuz  41492  jm2.23  41721  unxpwdom3  41823  hbtlem5  41856  fzunt  42192  fzuntd  42193  fzunt1d  42194  fzuntgd  42195  rp-fakeinunass  42252  sqrtcvallem1  42368  frege133d  42502  frege83  42683  frege131  42731  frege133  42733  uneqsn  42762  clsk1indlem3  42780  ntrneixb  42832  ntrneix3  42834  ntrneix13  42836  radcnvrat  43059  bccbc  43090  undif3VD  43629  iunconnlem2  43682  fnchoice  43699  limciccioolb  44324  limcicciooub  44340  icccncfext  44590  cncfiooicclem1  44596  fourierdlem70  44879  fourierdlem80  44889  fourierdlem93  44902  fourierdlem101  44910  sge0split  45112  el1fzopredsuc  46020  iccpartltu  46080  iccpartgtl  46081  iccpartgt  46082  iccpartleu  46083  iccpartgel  46084  fmtno4prmfac  46227  31prm  46252  sbgoldbo  46442  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  wtgoldbnnsum4prm  46457  bgoldbnnsum3prm  46459  bgoldbtbndlem3  46462  bgoldbtbnd  46464