Theorem elun 3976

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 3414	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3414	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3414	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 846	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2847	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2847	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 905	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3797	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3561	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 370	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 198   ∨ wo 836   = wceq 1601   ∈ wcel 2107  Vcvv 3398   ∪ cun 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-un 3797

This theorem is referenced by:  elunnel1  3977  uneqri  3978  uncom  3980  uneq1  3983  unass  3993  ssun1  3999  unss1  4005  ssequn1  4006  unss  4010  rexun  4016  ralunb  4017  elsymdif  4072  symdif2OLD  4080  indi  4100  undi  4101  unineq  4104  undif3  4115  rabun2  4132  reuun2  4136  undif4  4259  ssundif  4276  dfpr2  4417  elpwunsn  4452  eltpg  4454  pwpr  4667  pwtp  4668  uniun  4694  intun  4744  iinun2  4821  iunun  4840  iunxun  4841  iinuni  4845  brun  4939  pwunss  5258  pwssun  5259  opthprc  5415  xpundi  5419  xpundir  5420  difxp  5814  sossfld  5836  elsuci  6044  elsucg  6045  elsuc2g  6046  funun  6182  mptun  6273  unpreima  6607  suceloni  7293  ordsucun  7305  fnse  7577  reldmtpos  7644  dftpos4  7655  tpostpos  7656  wfrlem14  7713  wfrlem15  7714  oarec  7928  brdom2  8273  unxpdomlem3  8456  domunfican  8523  dfsup2  8640  wemapso2lem  8748  unwdomg  8780  unxpwdom2  8784  cantnfp1lem3  8876  rankunb  9012  djur  9080  djuunxp  9082  eldju2ndl  9085  eldju2ndr  9086  djuun  9087  iscard3  9251  kmlem2  9310  ssfin4  9469  dffin7-2  9557  fin1a2lem11  9569  fin1a2lem12  9570  cfpwsdom  9743  elgch  9781  fpwwe2lem13  9801  canthp1lem2  9812  gch2  9834  elnn0  11648  un0addcl  11681  un0mulcl  11682  elxnn0  11720  ltxr  12264  elxr  12265  xrsupexmnf  12451  xrinfmexpnf  12452  supxrun  12462  ixxun  12507  difreicc  12625  iccsplit  12626  fzsplit2  12687  elfzp1  12712  uzsplit  12734  elfzp12  12741  fzosplit  12824  fzouzsplit  12826  elfzonlteqm1  12867  elfzo0l  12881  fzosplitsni  12902  elfzr  12904  elfzlmr  12905  hashnn0pnf  13451  hashf1lem2  13558  hash2pwpr  13576  pr2pwpr  13579  ccatrn  13683  cats1un  13845  fsumsplit  14882  sumsplit  14908  fprodsplit  15103  rpnnen2lem12  15362  sumeven  15521  sumodd  15522  saddisjlem  15596  lcmfunsnlem1  15760  lcmfunsnlem2lem1  15761  lcmfunsnlem2lem2  15762  lcmfunsnlem2  15763  coprmprod  15784  coprmproddvdslem  15785  nnnn0modprm0  15919  prm23lt5  15927  vdwapun  16086  ramubcl  16130  basprssdmsets  16325  xpsfrnel2  16615  mreexmrid  16693  lubun  17513  symgextf1  18228  gsumzsplit  18717  gsumzunsnd  18745  gsumunsnfd  18746  dprddisj2  18829  dmdprdsplit2lem  18835  dmdprdsplit2  18836  dprdsplit  18838  mplcoe1  19866  mplcoe5  19869  evlslem4  19908  cnfldfunALT  20159  mdetunilem9  20835  maducoeval2  20855  madugsum  20858  clslp  21364  islpi  21365  restntr  21398  pnfnei  21436  mnfnei  21437  iunconn  21644  refun0  21731  xkoptsub  21870  ptunhmeo  22024  fbun  22056  filconn  22099  fixufil  22138  ufildr  22147  alexsubALTlem2  22264  alexsubALTlem3  22265  alexsubALTlem4  22266  tsmssplit  22367  xrtgioo  23021  reconnlem2  23042  iccpnfcnv  23155  iccpnfhmeo  23156  rrxcph  23602  rrxdstprj1  23619  mbfss  23854  mbfmax  23857  itg2splitlem  23956  itg2split  23957  iblss2  24013  itgsplit  24043  limcdif  24081  ellimc2  24082  limcmpt  24088  limcres  24091  limccnp  24096  limccnp2  24097  limcco  24098  rollelem  24193  dvivthlem1  24212  dvne0  24215  lhop  24220  degltlem1  24273  ply1rem  24364  fta1glem2  24367  plypf1  24409  plyaddlem1  24410  plymullem1  24411  plycj  24474  ofmulrt  24478  taylfval  24554  abelthlem2  24627  abelthlem3  24628  reasinsin  25078  scvxcvx  25168  ppinprm  25334  chtnprm  25336  dchrfi  25436  lgsdir2  25511  2lgslem3  25585  2lgsoddprmlem3  25595  usgrexmplef  26610  cffldtocusgr  26799  vtxdun  26833  eucrct2eupthOLD  27654  eucrct2eupth  27655  shunssi  28803  atomli  29817  atoml2i  29818  isoun  30049  fzsplit3  30121  eliccioo  30205  lindsun  30443  lbsdiflsp0  30444  ordtconnlem1  30572  xrge0iifcnv  30581  xrge0iifiso  30583  xrge0iifhom  30585  esumsplit  30717  esumpad2  30720  measvuni  30879  sxbrsigalem0  30935  bnj1138  31462  bnj1137  31666  subfacp1lem4  31768  subfacp1lem5  31769  kur14lem7  31797  mrsubcv  32010  mclsax  32069  dftrpred3g  32325  nosepdmlem  32426  brcup  32639  refssfne  32945  bj-eltag  33541  bj-0eltag  33542  bj-sngltag  33547  bj-projun  33558  tan2h  34031  poimirlem2  34042  poimirlem8  34048  poimirlem18  34058  poimirlem21  34061  poimirlem22  34062  poimirlem23  34063  poimirlem24  34064  poimirlem25  34065  poimirlem27  34067  poimirlem29  34069  poimirlem31  34071  poimirlem32  34072  ftc1anclem1  34115  ftc1anclem5  34119  dvasin  34126  dvacos  34127  eqfnun  34146  smprngopr  34480  elpadd  35958  paddval0  35969  hdmaplem4  37933  mapdh9a  37948  lzunuz  38301  jm2.23  38532  unxpwdom3  38634  hbtlem5  38667  rp-fakeinunass  38828  frege133d  39024  frege83  39206  frege131  39254  frege133  39256  uneqsn  39287  clsk1indlem3  39307  ntrneixb  39359  ntrneix3  39361  ntrneix13  39363  radcnvrat  39479  bccbc  39510  undif3VD  40061  iunconnlem2  40114  fnchoice  40131  elunnel2  40141  unima  40280  limciccioolb  40771  limcicciooub  40787  icccncfext  41038  cncfiooicclem1  41044  fourierdlem70  41330  fourierdlem80  41340  fourierdlem93  41353  fourierdlem101  41361  sge0split  41560  el1fzopredsuc  42377  iccpartltu  42403  iccpartgtl  42404  iccpartgt  42405  iccpartleu  42406  iccpartgel  42407  fmtno4prmfac  42515  31prm  42543  sbgoldbo  42710  nnsum4primeseven  42723  nnsum4primesevenALTV  42724  wtgoldbnnsum4prm  42725  bgoldbnnsum3prm  42727  bgoldbtbndlem3  42730  bgoldbtbnd  42732