MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elun Structured version   Visualization version   GIF version

Theorem elun 3619
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.
StepHypRef Expression
1 elex 3089 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3089 . . 3 (𝐴𝐵𝐴 ∈ V)
3 elex 3089 . . 3 (𝐴𝐶𝐴 ∈ V)
42, 3jaoi 392 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
5 eleq1 2580 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 eleq1 2580 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
75, 6orbi12d 741 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
8 df-un 3449 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
97, 8elab2g 3226 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
101, 4, 9pm5.21nii 366 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wo 381   = wceq 1474  wcel 1938  Vcvv 3077  cun 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-v 3079  df-un 3449
This theorem is referenced by:  elunnel1  3620  uneqri  3621  uncom  3623  uneq1  3626  unass  3636  ssun1  3642  unss1  3648  ssequn1  3649  unss  3653  rexun  3659  ralunb  3660  elsymdif  3714  symdif2  3717  indi  3735  undi  3736  unineq  3739  undif3  3750  undif3OLD  3751  rabun2  3768  reuun2  3772  undif4  3890  ssundif  3907  dfpr2  4046  elpwunsn  4074  eltpg  4077  pwpr  4266  pwtp  4267  uniun  4290  intun  4342  iinun2  4420  iunun  4438  iunxun  4439  iinuni  4443  brun  4531  pwunss  4837  pwssun  4838  opthprc  4983  xpundi  4988  xpundir  4989  difxp  5367  sossfld  5389  elsuci  5596  elsucg  5597  elsuc2g  5598  funun  5731  mptun  5823  unpreima  6132  suceloni  6780  ordsucun  6792  fnse  7055  reldmtpos  7121  dftpos4  7132  tpostpos  7133  wfrlem14  7189  wfrlem15  7190  oarec  7404  brdom2  7746  unxpdomlem3  7926  domunfican  7993  dfsup2  8108  wemapso2lem  8215  unwdomg  8247  unxpwdom2  8251  cantnfp1lem3  8335  rankunb  8471  iscard3  8674  kmlem2  8731  ssfin4  8890  dffin7-2  8978  fin1a2lem11  8990  fin1a2lem12  8991  cfpwsdom  9160  elgch  9198  fpwwe2lem13  9218  canthp1lem2  9229  gch2  9251  elnn0  11048  un0addcl  11080  un0mulcl  11081  ltxr  11693  elxr  11694  xrsupexmnf  11872  xrinfmexpnf  11873  supxrun  11883  ixxun  11930  difreicc  12043  iccsplit  12044  fzsplit2  12104  elfzp1  12128  uzsplit  12148  elfzp12  12155  fzosplit  12237  fzouzsplit  12239  elfzonlteqm1  12277  fzosplitsni  12311  hashnn0pnf  12856  hashf1lem2  12960  hash2pwpr  12976  pr2pwpr  12977  ccatrn  13082  cats1un  13184  fsumsplit  14185  sumsplit  14208  fprodsplit  14402  rpnnen2lem12  14660  sumeven  14815  sumodd  14816  saddisjlem  14895  lcmfunsnlem1  15062  lcmfunsnlem2lem1  15063  lcmfunsnlem2lem2  15064  lcmfunsnlem2  15065  coprmprod  15087  coprmproddvdslem  15088  nnnn0modprm0  15231  prm23lt5  15239  vdwapun  15398  ramubcl  15442  xpsfrnel2  15938  mreexmrid  16016  lubun  16836  symgextf1  17554  gsumzsplit  18055  gsumzunsnd  18083  gsumunsnfd  18084  dprddisj2  18166  dmdprdsplit2lem  18172  dmdprdsplit2  18173  dprdsplit  18175  mplcoe1  19188  mplcoe5  19191  evlslem4  19231  mdetunilem9  20146  maducoeval2  20166  madugsum  20169  clslp  20663  islpi  20664  restntr  20697  pnfnei  20735  mnfnei  20736  iuncon  20942  refun0  21029  xkoptsub  21168  ptunhmeo  21322  fbun  21355  filcon  21398  fixufil  21437  ufildr  21446  alexsubALTlem2  21563  alexsubALTlem3  21564  alexsubALTlem4  21565  tsmssplit  21666  xrtgioo  22324  reconnlem2  22345  iccpnfcnv  22472  iccpnfhmeo  22473  rrxcph  22852  rrxdstprj1  22864  mbfss  23095  mbfmax  23098  itg2splitlem  23197  itg2split  23198  iblss2  23254  itgsplit  23284  limcdif  23322  ellimc2  23323  limcmpt  23329  limcres  23332  limccnp  23337  limccnp2  23338  limcco  23339  rollelem  23432  dvivthlem1  23451  dvne0  23454  lhop  23459  degltlem1  23512  ply1rem  23605  fta1glem2  23608  plypf1  23657  plyaddlem1  23658  plymullem1  23659  plycj  23722  ofmulrt  23726  taylfval  23805  abelthlem2  23878  abelthlem3  23879  reasinsin  24311  scvxcvx  24400  ppinprm  24568  chtnprm  24570  dchrfi  24670  lgsdir2  24745  2lgslem3  24819  2lgsoddprmlem3  24829  usgraexmplef  25668  vdgrf  26164  vdgrun  26167  vdgrfiun  26168  vdgfrgragt2  26293  frgrawopreglem2  26311  shunssi  27400  atomli  28414  atoml2i  28415  isoun  28651  fzsplit3  28736  eliccioo  28766  ordtconlem1  29095  xrge0iifcnv  29104  xrge0iifiso  29106  xrge0iifhom  29108  esumsplit  29239  esumpad2  29242  measvuni  29401  sxbrsigalem0  29457  bnj1138  29959  bnj1137  30163  subfacp1lem4  30265  subfacp1lem5  30266  kur14lem7  30294  mrsubcv  30507  mclsax  30566  dftrpred3g  30820  brcup  31052  refssfne  31358  bj-eltag  31990  bj-0eltag  31991  bj-sngltag  31996  bj-projun  32007  tan2h  32446  poimirlem2  32456  poimirlem8  32462  poimirlem18  32472  poimirlem21  32475  poimirlem22  32476  poimirlem23  32477  poimirlem24  32478  poimirlem25  32479  poimirlem27  32481  poimirlem29  32483  poimirlem31  32485  poimirlem32  32486  ftc1anclem1  32530  ftc1anclem5  32534  dvasin  32541  dvacos  32542  eqfnun  32561  smprngopr  32896  elpadd  33978  paddval0  33989  hdmaplem4  35956  mapdh9a  35972  lzunuz  36224  jm2.23  36456  unxpwdom3  36558  hbtlem5  36592  rp-fakeinunass  36762  frege133d  36958  frege83  37142  frege131  37190  frege133  37192  uneqsn  37223  clsk1indlem3  37243  ntrneixb  37295  ntrneix3  37297  ntrneix13  37299  radcnvrat  37417  bccbc  37448  undif3VD  38022  iunconlem2  38075  fnchoice  38093  elunnel2  38103  unima  38223  limciccioolb  38574  limcicciooub  38590  icccncfext  38660  cncfiooicclem1  38666  fourierdlem70  38961  fourierdlem80  38971  fourierdlem93  38984  fourierdlem101  38992  sge0split  39196  el1fzopredsuc  39843  iccpartltu  39858  iccpartgtl  39859  iccpartgt  39860  iccpartleu  39861  iccpartgel  39862  fmtno4prmfac  39917  31prm  39945  nnsum4primeseven  40111  nnsum4primesevenALTV  40112  wtgoldbnnsum4prm  40113  bgoldbnnsum3prm  40115  bgoldbtbndlem3  40118  bgoldbtbnd  40120  elfzr  40281  elfzo0l  40282  elfzlmr  40283  elxnn0  40291  uhgrstrrepelem  40395  vtxdun  40788  eucrct2eupth  41505
  Copyright terms: Public domain W3C validator