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

Theorem elun 3601
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 3075 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3075 . . 3 (𝐴𝐵𝐴 ∈ V)
3 elex 3075 . . 3 (𝐴𝐶𝐴 ∈ V)
42, 3jaoi 388 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
5 eleq1 2571 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 eleq1 2571 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
75, 6orbi12d 733 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
8 df-un 3431 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
97, 8elab2g 3211 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
101, 4, 9pm5.21nii 362 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 191  wo 377   = wceq 1468  wcel 1937  Vcvv 3066  cun 3424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-v 3068  df-un 3431
This theorem is referenced by:  elunnel1  3602  uneqri  3603  uncom  3605  uneq1  3608  unass  3618  ssun1  3624  unss1  3630  ssequn1  3631  unss  3635  rexun  3641  ralunb  3642  elsymdif  3695  symdif2  3698  indi  3716  undi  3717  unineq  3720  undif3  3731  rabun2  3748  reuun2  3752  undif4  3861  ssundif  3878  dfpr2  4013  elpwunsn  4040  eltpg  4042  pwpr  4224  pwtp  4225  uniun  4247  intun  4296  iinun2  4373  iunun  4391  iunxun  4392  iinuni  4396  brun  4483  pwunss  4785  pwssun  4786  opthprc  4929  xpundi  4934  xpundir  4935  difxp  5311  sossfld  5333  elsuci  5540  elsucg  5541  elsuc2g  5542  funun  5675  mptun  5764  unpreima  6073  suceloni  6717  ordsucun  6729  fnse  6992  reldmtpos  7058  dftpos4  7069  tpostpos  7070  wfrlem14  7126  wfrlem15  7127  oarec  7340  brdom2  7682  unxpdomlem3  7862  domunfican  7929  dfsup2  8043  wemapso2lem  8150  unwdomg  8182  unxpwdom2  8186  cantnfp1lem3  8270  rankunb  8406  iscard3  8609  kmlem2  8666  ssfin4  8825  dffin7-2  8913  fin1a2lem11  8925  fin1a2lem12  8926  cfpwsdom  9094  elgch  9132  fpwwe2lem13  9152  canthp1lem2  9163  gch2  9185  elnn0  10962  un0addcl  10994  un0mulcl  10995  ltxr  11506  elxr  11507  xrsupexmnf  11685  xrinfmexpnf  11686  supxrun  11696  ixxun  11746  difreicc  11860  iccsplit  11861  fzsplit2  11920  elfzp1  11944  uzsplit  11964  elfzp12  11971  fzosplit  12052  fzouzsplit  12054  elfzonlteqm1  12092  fzosplitsni  12125  hashnn0pnf  12639  hashf1lem2  12742  hash2pwpr  12758  pr2pwpr  12759  ccatrn  12864  cats1un  12965  fsumsplit  13966  sumsplit  13989  fprodsplit  14180  rpnnen2  14438  saddisjlem  14600  lcmfunsnlem1  14772  lcmfunsnlem2lem1  14773  lcmfunsnlem2lem2  14774  lcmfunsnlem2  14775  coprmprod  14840  coprmproddvdslem  14841  nnnn0modprm0  14919  vdwapun  15086  ramubcl  15138  xpsfrnel2  15636  mreexmrid  15714  lubun  16534  symgextf1  17223  gsumzsplit  17721  gsumzunsnd  17749  gsumunsnfd  17750  dprddisj2  17832  dmdprdsplit2lem  17838  dmdprdsplit2  17839  dprdsplit  17841  mplcoe1  18848  mplcoe5  18851  evlslem4  18890  mdetunilem9  19803  maducoeval2  19823  madugsum  19826  clslp  20321  islpi  20322  restntr  20355  pnfnei  20393  mnfnei  20394  iuncon  20600  refun0  20687  xkoptsub  20826  ptunhmeo  20980  fbun  21013  filcon  21056  fixufil  21095  ufildr  21104  alexsubALTlem2  21221  alexsubALTlem3  21222  alexsubALTlem4  21223  tsmssplit  21324  xrtgioo  21982  reconnlem2  22003  iccpnfcnv  22130  iccpnfhmeo  22131  rrxcph  22510  rrxdstprj1  22522  mbfss  22763  mbfmax  22766  itg2splitlem  22867  itg2split  22868  iblss2  22924  itgsplit  22954  limcdif  22992  ellimc2  22993  limcmpt  22999  limcres  23002  limccnp  23007  limccnp2  23008  limcco  23009  rollelem  23102  dvivthlem1  23121  dvne0  23124  lhop  23129  degltlem1  23182  ply1rem  23275  fta1glem2  23278  plypf1  23327  plyaddlem1  23328  plymullem1  23329  plycj  23392  ofmulrt  23396  taylfval  23475  abelthlem2  23548  abelthlem3  23549  reasinsin  23983  scvxcvx  24072  ppinprm  24240  chtnprm  24242  dchrfi  24344  lgsdir2  24417  usgraexmplef  25289  vdgrf  25786  vdgrun  25789  vdgrfiun  25790  vdgfrgragt2  25915  frgrawopreglem2  25933  shunssi  27184  atomli  28198  atoml2i  28199  isoun  28439  fzsplit3  28526  eliccioo  28556  ordtconlem1  28885  xrge0iifcnv  28894  xrge0iifiso  28896  xrge0iifhom  28898  esumsplit  29029  esumpad2  29032  measvuni  29191  sxbrsigalem0  29247  bnj1138  29752  bnj1137  29956  subfacp1lem4  30058  subfacp1lem5  30059  kur14lem7  30087  mrsubcv  30300  mclsax  30359  dftrpred3g  30625  brcup  30857  refssfne  31163  bj-eltag  31757  bj-0eltag  31758  bj-sngltag  31763  bj-projun  31774  tan2h  32170  poimirlem2  32180  poimirlem8  32186  poimirlem18  32196  poimirlem21  32199  poimirlem22  32200  poimirlem23  32201  poimirlem24  32202  poimirlem25  32203  poimirlem27  32205  poimirlem29  32207  poimirlem31  32209  poimirlem32  32210  ftc1anclem1  32255  ftc1anclem5  32259  dvasin  32266  dvacos  32267  eqfnun  32286  smprngopr  32522  elpadd  33604  paddval0  33615  hdmaplem4  35582  mapdh9a  35598  lzunuz  35850  jm2.23  36091  unxpwdom3  36193  hbtlem5  36227  rp-fakeinunass  36400  frege133d  36596  frege83  36781  frege131  36829  frege133  36831  ntrneixb  36906  radcnvrat  37020  bccbc  37051  undif3VD  37627  iunconlem2  37680  fnchoice  37698  elunnel2  37708  unima  37792  limciccioolb  38105  limcicciooub  38121  icccncfext  38174  cncfiooicclem1  38180  fourierdlem70  38476  fourierdlem80  38486  fourierdlem93  38499  fourierdlem101  38507  sge0split  38697  el1fzopredsuc  39242  iccpartltu  39259  iccpartgtl  39260  iccpartgt  39261  iccpartleu  39262  iccpartgel  39263  nnsum4primeseven  39415  nnsum4primesevenALTV  39416  wtgoldbnnsum4prm  39417  bgoldbnnsum3prm  39419  bgoldbtbndlem3  39422  bgoldbtbnd  39424  elfzr  39589  elfzo0l  39590  elfzlmr  39591  elxnn0  39599  uhgrstrrepelem  39703  vtxdun  40096  eucrct2eupth  40813
  Copyright terms: Public domain W3C validator