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

Theorem elun 3714
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 3184 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3184 . . 3 (𝐴𝐵𝐴 ∈ V)
3 elex 3184 . . 3 (𝐴𝐶𝐴 ∈ V)
42, 3jaoi 392 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
5 eleq1 2675 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 eleq1 2675 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
75, 6orbi12d 741 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
8 df-un 3544 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
97, 8elab2g 3321 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
101, 4, 9pm5.21nii 366 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wo 381   = wceq 1474  wcel 1976  Vcvv 3172  cun 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544
This theorem is referenced by:  elunnel1  3715  uneqri  3716  uncom  3718  uneq1  3721  unass  3731  ssun1  3737  unss1  3743  ssequn1  3744  unss  3748  rexun  3754  ralunb  3755  elsymdif  3810  symdif2  3813  indi  3831  undi  3832  unineq  3835  undif3  3846  undif3OLD  3847  rabun2  3864  reuun2  3868  undif4  3986  ssundif  4003  dfpr2  4142  elpwunsn  4170  eltpg  4173  pwpr  4362  pwtp  4363  uniun  4386  intun  4438  iinun2  4516  iunun  4534  iunxun  4535  iinuni  4539  brun  4627  pwunss  4933  pwssun  4934  opthprc  5079  xpundi  5084  xpundir  5085  difxp  5463  sossfld  5485  elsuci  5694  elsucg  5695  elsuc2g  5696  funun  5832  mptun  5924  unpreima  6234  suceloni  6882  ordsucun  6894  fnse  7158  reldmtpos  7224  dftpos4  7235  tpostpos  7236  wfrlem14  7292  wfrlem15  7293  oarec  7506  brdom2  7848  unxpdomlem3  8028  domunfican  8095  dfsup2  8210  wemapso2lem  8317  unwdomg  8349  unxpwdom2  8353  cantnfp1lem3  8437  rankunb  8573  iscard3  8776  kmlem2  8833  ssfin4  8992  dffin7-2  9080  fin1a2lem11  9092  fin1a2lem12  9093  cfpwsdom  9262  elgch  9300  fpwwe2lem13  9320  canthp1lem2  9331  gch2  9353  elnn0  11141  un0addcl  11173  un0mulcl  11174  ltxr  11784  elxr  11785  xrsupexmnf  11963  xrinfmexpnf  11964  supxrun  11974  ixxun  12018  difreicc  12131  iccsplit  12132  fzsplit2  12192  elfzp1  12216  uzsplit  12236  elfzp12  12243  fzosplit  12325  fzouzsplit  12327  elfzonlteqm1  12365  fzosplitsni  12399  hashnn0pnf  12944  hashf1lem2  13049  hash2pwpr  13065  pr2pwpr  13066  ccatrn  13171  cats1un  13273  fsumsplit  14264  sumsplit  14287  fprodsplit  14481  rpnnen2lem12  14739  sumeven  14894  sumodd  14895  saddisjlem  14970  lcmfunsnlem1  15134  lcmfunsnlem2lem1  15135  lcmfunsnlem2lem2  15136  lcmfunsnlem2  15137  coprmprod  15159  coprmproddvdslem  15160  nnnn0modprm0  15295  prm23lt5  15303  vdwapun  15462  ramubcl  15506  xpsfrnel2  15994  mreexmrid  16072  lubun  16892  symgextf1  17610  gsumzsplit  18096  gsumzunsnd  18124  gsumunsnfd  18125  dprddisj2  18207  dmdprdsplit2lem  18213  dmdprdsplit2  18214  dprdsplit  18216  mplcoe1  19232  mplcoe5  19235  evlslem4  19275  mdetunilem9  20187  maducoeval2  20207  madugsum  20210  clslp  20704  islpi  20705  restntr  20738  pnfnei  20776  mnfnei  20777  iuncon  20983  refun0  21070  xkoptsub  21209  ptunhmeo  21363  fbun  21396  filcon  21439  fixufil  21478  ufildr  21487  alexsubALTlem2  21604  alexsubALTlem3  21605  alexsubALTlem4  21606  tsmssplit  21707  xrtgioo  22349  reconnlem2  22370  iccpnfcnv  22482  iccpnfhmeo  22483  rrxcph  22905  rrxdstprj1  22917  mbfss  23136  mbfmax  23139  itg2splitlem  23238  itg2split  23239  iblss2  23295  itgsplit  23325  limcdif  23363  ellimc2  23364  limcmpt  23370  limcres  23373  limccnp  23378  limccnp2  23379  limcco  23380  rollelem  23473  dvivthlem1  23492  dvne0  23495  lhop  23500  degltlem1  23553  ply1rem  23644  fta1glem2  23647  plypf1  23689  plyaddlem1  23690  plymullem1  23691  plycj  23754  ofmulrt  23758  taylfval  23834  abelthlem2  23907  abelthlem3  23908  reasinsin  24340  scvxcvx  24429  ppinprm  24595  chtnprm  24597  dchrfi  24697  lgsdir2  24772  2lgslem3  24846  2lgsoddprmlem3  24856  usgraexmplef  25695  vdgrf  26191  vdgrun  26194  vdgrfiun  26195  vdgfrgragt2  26320  frgrawopreglem2  26338  shunssi  27417  atomli  28431  atoml2i  28432  isoun  28668  fzsplit3  28746  eliccioo  28776  ordtconlem1  29104  xrge0iifcnv  29113  xrge0iifiso  29115  xrge0iifhom  29117  esumsplit  29248  esumpad2  29251  measvuni  29410  sxbrsigalem0  29466  bnj1138  29919  bnj1137  30123  subfacp1lem4  30225  subfacp1lem5  30226  kur14lem7  30254  mrsubcv  30467  mclsax  30526  dftrpred3g  30783  brcup  31022  refssfne  31329  bj-eltag  31961  bj-0eltag  31962  bj-sngltag  31967  bj-projun  31978  tan2h  32374  poimirlem2  32384  poimirlem8  32390  poimirlem18  32400  poimirlem21  32403  poimirlem22  32404  poimirlem23  32405  poimirlem24  32406  poimirlem25  32407  poimirlem27  32409  poimirlem29  32411  poimirlem31  32413  poimirlem32  32414  ftc1anclem1  32458  ftc1anclem5  32462  dvasin  32469  dvacos  32470  eqfnun  32489  smprngopr  32824  elpadd  33906  paddval0  33917  hdmaplem4  35884  mapdh9a  35900  lzunuz  36152  jm2.23  36384  unxpwdom3  36486  hbtlem5  36520  rp-fakeinunass  36683  frege133d  36879  frege83  37063  frege131  37111  frege133  37113  uneqsn  37144  clsk1indlem3  37164  ntrneixb  37216  ntrneix3  37218  ntrneix13  37220  radcnvrat  37338  bccbc  37369  undif3VD  37943  iunconlem2  37996  fnchoice  38014  elunnel2  38024  unima  38143  limciccioolb  38492  limcicciooub  38508  icccncfext  38577  cncfiooicclem1  38583  fourierdlem70  38873  fourierdlem80  38883  fourierdlem93  38896  fourierdlem101  38904  sge0split  39106  el1fzopredsuc  39753  iccpartltu  39768  iccpartgtl  39769  iccpartgt  39770  iccpartleu  39771  iccpartgel  39772  fmtno4prmfac  39827  31prm  39855  nnsum4primeseven  40021  nnsum4primesevenALTV  40022  wtgoldbnnsum4prm  40023  bgoldbnnsum3prm  40025  bgoldbtbndlem3  40028  bgoldbtbnd  40030  elfzr  40191  elfzo0l  40192  elfzlmr  40193  elxnn0  40201  uhgrstrrepelem  40305  vtxdun  40698  eucrct2eupth  41415
  Copyright terms: Public domain W3C validator