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

Theorem elun 3884
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 3340 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3340 . . 3 (𝐴𝐵𝐴 ∈ V)
3 elex 3340 . . 3 (𝐴𝐶𝐴 ∈ V)
42, 3jaoi 393 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
5 eleq1 2815 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 eleq1 2815 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
75, 6orbi12d 748 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
8 df-un 3708 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
97, 8elab2g 3481 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
101, 4, 9pm5.21nii 367 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 382   = wceq 1620  wcel 2127  Vcvv 3328  cun 3701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330  df-un 3708
This theorem is referenced by:  elunnel1  3885  uneqri  3886  uncom  3888  uneq1  3891  unass  3901  ssun1  3907  unss1  3913  ssequn1  3914  unss  3918  rexun  3924  ralunb  3925  elsymdif  3980  symdif2  3983  indi  4004  undi  4005  unineq  4008  undif3  4019  undif3OLD  4020  rabun2  4037  reuun2  4041  undif4  4167  ssundif  4184  dfpr2  4327  elpwunsn  4356  eltpg  4359  pwpr  4570  pwtp  4571  uniun  4596  intun  4649  iinun2  4726  iunun  4744  iunxun  4745  iinuni  4749  brun  4843  pwunss  5157  pwssun  5158  opthprc  5312  xpundi  5316  xpundir  5317  difxp  5704  sossfld  5726  elsuci  5940  elsucg  5941  elsuc2g  5942  funun  6081  mptun  6174  unpreima  6492  suceloni  7166  ordsucun  7178  fnse  7450  reldmtpos  7517  dftpos4  7528  tpostpos  7529  wfrlem14  7585  wfrlem15  7586  oarec  7799  brdom2  8139  unxpdomlem3  8319  domunfican  8386  dfsup2  8503  wemapso2lem  8610  unwdomg  8642  unxpwdom2  8646  cantnfp1lem3  8738  rankunb  8874  iscard3  9077  kmlem2  9136  ssfin4  9295  dffin7-2  9383  fin1a2lem11  9395  fin1a2lem12  9396  cfpwsdom  9569  elgch  9607  fpwwe2lem13  9627  canthp1lem2  9638  gch2  9660  elnn0  11457  un0addcl  11489  un0mulcl  11490  elxnn0  11528  ltxr  12113  elxr  12114  xrsupexmnf  12299  xrinfmexpnf  12300  supxrun  12310  ixxun  12355  difreicc  12468  iccsplit  12469  fzsplit2  12530  elfzp1  12555  uzsplit  12576  elfzp12  12583  fzosplit  12666  fzouzsplit  12668  elfzonlteqm1  12709  elfzo0l  12723  fzosplitsni  12744  elfzr  12746  elfzlmr  12747  hashnn0pnf  13295  hashf1lem2  13403  hash2pwpr  13421  pr2pwpr  13424  ccatrn  13532  cats1un  13646  fsumsplit  14641  sumsplit  14669  fprodsplit  14866  rpnnen2lem12  15124  sumeven  15283  sumodd  15284  saddisjlem  15359  lcmfunsnlem1  15523  lcmfunsnlem2lem1  15524  lcmfunsnlem2lem2  15525  lcmfunsnlem2  15526  coprmprod  15548  coprmproddvdslem  15549  nnnn0modprm0  15684  prm23lt5  15692  vdwapun  15851  ramubcl  15895  basprssdmsets  16098  xpsfrnel2  16398  mreexmrid  16476  lubun  17295  symgextf1  18012  gsumzsplit  18498  gsumzunsnd  18526  gsumunsnfd  18527  dprddisj2  18609  dmdprdsplit2lem  18615  dmdprdsplit2  18616  dprdsplit  18618  mplcoe1  19638  mplcoe5  19641  evlslem4  19681  cnfldfunALT  19932  mdetunilem9  20599  maducoeval2  20619  madugsum  20622  clslp  21125  islpi  21126  restntr  21159  pnfnei  21197  mnfnei  21198  iunconn  21404  refun0  21491  xkoptsub  21630  ptunhmeo  21784  fbun  21816  filconn  21859  fixufil  21898  ufildr  21907  alexsubALTlem2  22024  alexsubALTlem3  22025  alexsubALTlem4  22026  tsmssplit  22127  xrtgioo  22781  reconnlem2  22802  iccpnfcnv  22915  iccpnfhmeo  22916  rrxcph  23351  rrxdstprj1  23363  mbfss  23583  mbfmax  23586  itg2splitlem  23685  itg2split  23686  iblss2  23742  itgsplit  23772  limcdif  23810  ellimc2  23811  limcmpt  23817  limcres  23820  limccnp  23825  limccnp2  23826  limcco  23827  rollelem  23922  dvivthlem1  23941  dvne0  23944  lhop  23949  degltlem1  24002  ply1rem  24093  fta1glem2  24096  plypf1  24138  plyaddlem1  24139  plymullem1  24140  plycj  24203  ofmulrt  24207  taylfval  24283  abelthlem2  24356  abelthlem3  24357  reasinsin  24793  scvxcvx  24882  ppinprm  25048  chtnprm  25050  dchrfi  25150  lgsdir2  25225  2lgslem3  25299  2lgsoddprmlem3  25309  usgrexmplef  26321  cffldtocusgr  26524  vtxdun  26558  eucrct2eupth  27368  shunssi  28507  atomli  29521  atoml2i  29522  isoun  29759  fzsplit3  29833  eliccioo  29919  ordtconnlem1  30250  xrge0iifcnv  30259  xrge0iifiso  30261  xrge0iifhom  30263  esumsplit  30395  esumpad2  30398  measvuni  30557  sxbrsigalem0  30613  bnj1138  31137  bnj1137  31341  subfacp1lem4  31443  subfacp1lem5  31444  kur14lem7  31472  mrsubcv  31685  mclsax  31744  dftrpred3g  32009  nosepdmlem  32110  brcup  32323  refssfne  32630  bj-eltag  33242  bj-0eltag  33243  bj-sngltag  33248  bj-projun  33259  tan2h  33683  poimirlem2  33693  poimirlem8  33699  poimirlem18  33709  poimirlem21  33712  poimirlem22  33713  poimirlem23  33714  poimirlem24  33715  poimirlem25  33716  poimirlem27  33718  poimirlem29  33720  poimirlem31  33722  poimirlem32  33723  ftc1anclem1  33767  ftc1anclem5  33771  dvasin  33778  dvacos  33779  eqfnun  33798  smprngopr  34133  elpadd  35557  paddval0  35568  hdmaplem4  37534  mapdh9a  37550  lzunuz  37802  jm2.23  38034  unxpwdom3  38136  hbtlem5  38169  rp-fakeinunass  38332  frege133d  38528  frege83  38711  frege131  38759  frege133  38761  uneqsn  38792  clsk1indlem3  38812  ntrneixb  38864  ntrneix3  38866  ntrneix13  38868  radcnvrat  38984  bccbc  39015  undif3VD  39586  iunconnlem2  39639  fnchoice  39656  elunnel2  39666  unima  39814  limciccioolb  40325  limcicciooub  40341  icccncfext  40572  cncfiooicclem1  40578  fourierdlem70  40865  fourierdlem80  40875  fourierdlem93  40888  fourierdlem101  40896  sge0split  41098  el1fzopredsuc  41814  iccpartltu  41840  iccpartgtl  41841  iccpartgt  41842  iccpartleu  41843  iccpartgel  41844  fmtno4prmfac  41963  31prm  41991  sbgoldbo  42154  nnsum4primeseven  42167  nnsum4primesevenALTV  42168  wtgoldbnnsum4prm  42169  bgoldbnnsum3prm  42171  bgoldbtbndlem3  42174  bgoldbtbnd  42176
  Copyright terms: Public domain W3C validator