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

Theorem elun 3715
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 3185 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3185 . . 3 (𝐴𝐵𝐴 ∈ V)
3 elex 3185 . . 3 (𝐴𝐶𝐴 ∈ V)
42, 3jaoi 393 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
5 eleq1 2676 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 eleq1 2676 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
75, 6orbi12d 742 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
8 df-un 3545 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
97, 8elab2g 3322 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
101, 4, 9pm5.21nii 367 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wo 382   = wceq 1475  wcel 1977  Vcvv 3173  cun 3538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545
This theorem is referenced by:  elunnel1  3716  uneqri  3717  uncom  3719  uneq1  3722  unass  3732  ssun1  3738  unss1  3744  ssequn1  3745  unss  3749  rexun  3755  ralunb  3756  elsymdif  3811  symdif2  3814  indi  3832  undi  3833  unineq  3836  undif3  3847  undif3OLD  3848  rabun2  3865  reuun2  3869  undif4  3987  ssundif  4004  dfpr2  4143  elpwunsn  4171  eltpg  4174  pwpr  4368  pwtp  4369  uniun  4392  intun  4444  iinun2  4522  iunun  4540  iunxun  4541  iinuni  4545  brun  4633  pwunss  4943  pwssun  4944  opthprc  5089  xpundi  5094  xpundir  5095  difxp  5477  sossfld  5499  elsuci  5708  elsucg  5709  elsuc2g  5710  funun  5846  mptun  5938  unpreima  6249  suceloni  6905  ordsucun  6917  fnse  7181  reldmtpos  7247  dftpos4  7258  tpostpos  7259  wfrlem14  7315  wfrlem15  7316  oarec  7529  brdom2  7871  unxpdomlem3  8051  domunfican  8118  dfsup2  8233  wemapso2lem  8340  unwdomg  8372  unxpwdom2  8376  cantnfp1lem3  8460  rankunb  8596  iscard3  8799  kmlem2  8856  ssfin4  9015  dffin7-2  9103  fin1a2lem11  9115  fin1a2lem12  9116  cfpwsdom  9285  elgch  9323  fpwwe2lem13  9343  canthp1lem2  9354  gch2  9376  elnn0  11171  un0addcl  11203  un0mulcl  11204  elxnn0  11242  ltxr  11825  elxr  11826  xrsupexmnf  12007  xrinfmexpnf  12008  supxrun  12018  ixxun  12062  difreicc  12175  iccsplit  12176  fzsplit2  12237  elfzp1  12261  uzsplit  12281  elfzp12  12288  fzosplit  12370  fzouzsplit  12372  elfzonlteqm1  12410  fzosplitsni  12444  hashnn0pnf  12992  hashf1lem2  13097  hash2pwpr  13115  pr2pwpr  13116  ccatrn  13225  cats1un  13327  fsumsplit  14318  sumsplit  14341  fprodsplit  14535  rpnnen2lem12  14793  sumeven  14948  sumodd  14949  saddisjlem  15024  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  lcmfunsnlem2  15191  coprmprod  15213  coprmproddvdslem  15214  nnnn0modprm0  15349  prm23lt5  15357  vdwapun  15516  ramubcl  15560  xpsfrnel2  16048  mreexmrid  16126  lubun  16946  symgextf1  17664  gsumzsplit  18150  gsumzunsnd  18178  gsumunsnfd  18179  dprddisj2  18261  dmdprdsplit2lem  18267  dmdprdsplit2  18268  dprdsplit  18270  mplcoe1  19286  mplcoe5  19289  evlslem4  19329  mdetunilem9  20245  maducoeval2  20265  madugsum  20268  clslp  20762  islpi  20763  restntr  20796  pnfnei  20834  mnfnei  20835  iuncon  21041  refun0  21128  xkoptsub  21267  ptunhmeo  21421  fbun  21454  filcon  21497  fixufil  21536  ufildr  21545  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  tsmssplit  21765  xrtgioo  22417  reconnlem2  22438  iccpnfcnv  22551  iccpnfhmeo  22552  rrxcph  22988  rrxdstprj1  23000  mbfss  23219  mbfmax  23222  itg2splitlem  23321  itg2split  23322  iblss2  23378  itgsplit  23408  limcdif  23446  ellimc2  23447  limcmpt  23453  limcres  23456  limccnp  23461  limccnp2  23462  limcco  23463  rollelem  23556  dvivthlem1  23575  dvne0  23578  lhop  23583  degltlem1  23636  ply1rem  23727  fta1glem2  23730  plypf1  23772  plyaddlem1  23773  plymullem1  23774  plycj  23837  ofmulrt  23841  taylfval  23917  abelthlem2  23990  abelthlem3  23991  reasinsin  24423  scvxcvx  24512  ppinprm  24678  chtnprm  24680  dchrfi  24780  lgsdir2  24855  2lgslem3  24929  2lgsoddprmlem3  24939  uhgrstrrepelem  25744  usgraexmplef  25929  vdgrf  26425  vdgrun  26428  vdgrfiun  26429  vdgfrgragt2  26554  frgrawopreglem2  26572  shunssi  27611  atomli  28625  atoml2i  28626  isoun  28862  fzsplit3  28940  eliccioo  28970  ordtconlem1  29298  xrge0iifcnv  29307  xrge0iifiso  29309  xrge0iifhom  29311  esumsplit  29442  esumpad2  29445  measvuni  29604  sxbrsigalem0  29660  bnj1138  30113  bnj1137  30317  subfacp1lem4  30419  subfacp1lem5  30420  kur14lem7  30448  mrsubcv  30661  mclsax  30720  dftrpred3g  30977  brcup  31216  refssfne  31523  bj-eltag  32158  bj-0eltag  32159  bj-sngltag  32164  bj-projun  32175  tan2h  32571  poimirlem2  32581  poimirlem8  32587  poimirlem18  32597  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem27  32606  poimirlem29  32608  poimirlem31  32610  poimirlem32  32611  ftc1anclem1  32655  ftc1anclem5  32659  dvasin  32666  dvacos  32667  eqfnun  32686  smprngopr  33021  elpadd  34103  paddval0  34114  hdmaplem4  36081  mapdh9a  36097  lzunuz  36349  jm2.23  36581  unxpwdom3  36683  hbtlem5  36717  rp-fakeinunass  36880  frege133d  37076  frege83  37260  frege131  37308  frege133  37310  uneqsn  37341  clsk1indlem3  37361  ntrneixb  37413  ntrneix3  37415  ntrneix13  37417  radcnvrat  37535  bccbc  37566  undif3VD  38140  iunconlem2  38193  fnchoice  38211  elunnel2  38221  unima  38340  limciccioolb  38688  limcicciooub  38704  icccncfext  38773  cncfiooicclem1  38779  fourierdlem70  39069  fourierdlem80  39079  fourierdlem93  39092  fourierdlem101  39100  sge0split  39302  el1fzopredsuc  39948  iccpartltu  39963  iccpartgtl  39964  iccpartgt  39965  iccpartleu  39966  iccpartgel  39967  fmtno4prmfac  40022  31prm  40050  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  bgoldbtbndlem3  40223  bgoldbtbnd  40225  elfzr  40364  elfzo0l  40365  elfzlmr  40366  vtxdun  40696  eucrct2eupth  41413
  Copyright terms: Public domain W3C validator