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

Theorem elun 3731
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 3198 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3198 . . 3 (𝐴𝐵𝐴 ∈ V)
3 elex 3198 . . 3 (𝐴𝐶𝐴 ∈ V)
42, 3jaoi 394 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
5 eleq1 2686 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 eleq1 2686 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
75, 6orbi12d 745 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
8 df-un 3560 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
97, 8elab2g 3336 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
101, 4, 9pm5.21nii 368 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 383   = wceq 1480  wcel 1987  Vcvv 3186  cun 3553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3560
This theorem is referenced by:  elunnel1  3732  uneqri  3733  uncom  3735  uneq1  3738  unass  3748  ssun1  3754  unss1  3760  ssequn1  3761  unss  3765  rexun  3771  ralunb  3772  elsymdif  3827  symdif2  3830  indi  3849  undi  3850  unineq  3853  undif3  3864  undif3OLD  3865  rabun2  3882  reuun2  3886  undif4  4007  ssundif  4024  dfpr2  4166  elpwunsn  4195  eltpg  4198  pwpr  4398  pwtp  4399  uniun  4422  intun  4474  iinun2  4552  iunun  4570  iunxun  4571  iinuni  4575  brun  4663  pwunss  4979  pwssun  4980  opthprc  5127  xpundi  5132  xpundir  5133  difxp  5517  sossfld  5539  elsuci  5750  elsucg  5751  elsuc2g  5752  funun  5890  mptun  5982  unpreima  6297  suceloni  6960  ordsucun  6972  fnse  7239  reldmtpos  7305  dftpos4  7316  tpostpos  7317  wfrlem14  7373  wfrlem15  7374  oarec  7587  brdom2  7929  unxpdomlem3  8110  domunfican  8177  dfsup2  8294  wemapso2lem  8401  unwdomg  8433  unxpwdom2  8437  cantnfp1lem3  8521  rankunb  8657  iscard3  8860  kmlem2  8917  ssfin4  9076  dffin7-2  9164  fin1a2lem11  9176  fin1a2lem12  9177  cfpwsdom  9350  elgch  9388  fpwwe2lem13  9408  canthp1lem2  9419  gch2  9441  elnn0  11238  un0addcl  11270  un0mulcl  11271  elxnn0  11309  ltxr  11893  elxr  11894  xrsupexmnf  12078  xrinfmexpnf  12079  supxrun  12089  ixxun  12133  difreicc  12246  iccsplit  12247  fzsplit2  12308  elfzp1  12333  uzsplit  12353  elfzp12  12360  fzosplit  12442  fzouzsplit  12444  elfzonlteqm1  12484  elfzo0l  12499  fzosplitsni  12519  elfzr  12521  elfzlmr  12522  hashnn0pnf  13070  hashf1lem2  13178  hash2pwpr  13196  pr2pwpr  13199  ccatrn  13311  cats1un  13413  fsumsplit  14404  sumsplit  14427  fprodsplit  14621  rpnnen2lem12  14879  sumeven  15034  sumodd  15035  saddisjlem  15110  lcmfunsnlem1  15274  lcmfunsnlem2lem1  15275  lcmfunsnlem2lem2  15276  lcmfunsnlem2  15277  coprmprod  15299  coprmproddvdslem  15300  nnnn0modprm0  15435  prm23lt5  15443  vdwapun  15602  ramubcl  15646  basprssdmsets  15846  xpsfrnel2  16146  mreexmrid  16224  lubun  17044  symgextf1  17762  gsumzsplit  18248  gsumzunsnd  18276  gsumunsnfd  18277  dprddisj2  18359  dmdprdsplit2lem  18365  dmdprdsplit2  18366  dprdsplit  18368  mplcoe1  19384  mplcoe5  19387  evlslem4  19427  cnfldfunALT  19678  mdetunilem9  20345  maducoeval2  20365  madugsum  20368  clslp  20862  islpi  20863  restntr  20896  pnfnei  20934  mnfnei  20935  iunconn  21141  refun0  21228  xkoptsub  21367  ptunhmeo  21521  fbun  21554  filconn  21597  fixufil  21636  ufildr  21645  alexsubALTlem2  21762  alexsubALTlem3  21763  alexsubALTlem4  21764  tsmssplit  21865  xrtgioo  22517  reconnlem2  22538  iccpnfcnv  22651  iccpnfhmeo  22652  rrxcph  23088  rrxdstprj1  23100  mbfss  23319  mbfmax  23322  itg2splitlem  23421  itg2split  23422  iblss2  23478  itgsplit  23508  limcdif  23546  ellimc2  23547  limcmpt  23553  limcres  23556  limccnp  23561  limccnp2  23562  limcco  23563  rollelem  23656  dvivthlem1  23675  dvne0  23678  lhop  23683  degltlem1  23736  ply1rem  23827  fta1glem2  23830  plypf1  23872  plyaddlem1  23873  plymullem1  23874  plycj  23937  ofmulrt  23941  taylfval  24017  abelthlem2  24090  abelthlem3  24091  reasinsin  24523  scvxcvx  24612  ppinprm  24778  chtnprm  24780  dchrfi  24880  lgsdir2  24955  2lgslem3  25029  2lgsoddprmlem3  25039  usgrexmplef  26044  cffldtocusgr  26230  vtxdun  26263  eucrct2eupth  26971  shunssi  28073  atomli  29087  atoml2i  29088  isoun  29319  fzsplit3  29391  eliccioo  29421  ordtconnlem1  29749  xrge0iifcnv  29758  xrge0iifiso  29760  xrge0iifhom  29762  esumsplit  29893  esumpad2  29896  measvuni  30055  sxbrsigalem0  30111  bnj1138  30564  bnj1137  30768  subfacp1lem4  30870  subfacp1lem5  30871  kur14lem7  30899  mrsubcv  31112  mclsax  31171  dftrpred3g  31431  nosepdmlem  31564  brcup  31685  refssfne  31992  bj-eltag  32609  bj-0eltag  32610  bj-sngltag  32615  bj-projun  32626  tan2h  33030  poimirlem2  33040  poimirlem8  33046  poimirlem18  33056  poimirlem21  33059  poimirlem22  33060  poimirlem23  33061  poimirlem24  33062  poimirlem25  33063  poimirlem27  33065  poimirlem29  33067  poimirlem31  33069  poimirlem32  33070  ftc1anclem1  33114  ftc1anclem5  33118  dvasin  33125  dvacos  33126  eqfnun  33145  smprngopr  33480  elpadd  34562  paddval0  34573  hdmaplem4  36540  mapdh9a  36556  lzunuz  36808  jm2.23  37040  unxpwdom3  37142  hbtlem5  37176  rp-fakeinunass  37339  frege133d  37535  frege83  37719  frege131  37767  frege133  37769  uneqsn  37800  clsk1indlem3  37820  ntrneixb  37872  ntrneix3  37874  ntrneix13  37876  radcnvrat  37992  bccbc  38023  undif3VD  38598  iunconnlem2  38651  fnchoice  38668  elunnel2  38678  unima  38816  limciccioolb  39254  limcicciooub  39270  icccncfext  39401  cncfiooicclem1  39407  fourierdlem70  39697  fourierdlem80  39707  fourierdlem93  39720  fourierdlem101  39728  sge0split  39930  el1fzopredsuc  40629  iccpartltu  40656  iccpartgtl  40657  iccpartgt  40658  iccpartleu  40659  iccpartgel  40660  fmtno4prmfac  40780  31prm  40808  nnsum4primeseven  40974  nnsum4primesevenALTV  40975  wtgoldbnnsum4prm  40976  bgoldbnnsum3prm  40978  bgoldbtbndlem3  40981  bgoldbtbnd  40983
  Copyright terms: Public domain W3C validator