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

Theorem elun 4124
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 3512 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3512 . . 3 (𝐴𝐵𝐴 ∈ V)
3 elex 3512 . . 3 (𝐴𝐶𝐴 ∈ V)
42, 3jaoi 853 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
5 eleq1 2900 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 eleq1 2900 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
75, 6orbi12d 915 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
8 df-un 3940 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
97, 8elab2g 3667 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
101, 4, 9pm5.21nii 382 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wo 843   = wceq 1533  wcel 2110  Vcvv 3494  cun 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940
This theorem is referenced by:  elunnel1  4125  uneqri  4126  uncom  4128  uneq1  4131  unass  4141  ssun1  4147  elunant  4153  unss1  4154  ssequn1  4155  rexun  4165  elsymdif  4223  indi  4249  undi  4250  unineq  4253  undif3  4264  rabun2  4281  reuun2  4285  undif4  4415  ssundif  4432  dfpr2  4585  elpwunsn  4620  eltpg  4622  pwpr  4831  pwtp  4832  uniun  4860  iinun2  4994  iunun  5014  iunxun  5015  iinuni  5019  brun  5116  pwunssOLD  5454  pwssun  5455  opthprc  5615  xpundi  5619  xpundir  5620  difxp  6020  sossfld  6042  elsuci  6256  elsucg  6257  elsuc2g  6258  funun  6399  mptun  6493  unima  6738  unpreima  6832  suceloni  7527  ordsucun  7539  fnse  7826  suppofssd  7866  reldmtpos  7899  dftpos4  7910  tpostpos  7911  wfrlem14  7967  wfrlem15  7968  oarec  8187  brdom2  8538  unxpdomlem3  8723  domunfican  8790  dfsup2  8907  wemapso2lem  9015  unwdomg  9047  unxpwdom2  9051  cantnfp1lem3  9142  rankunb  9278  djur  9347  djuunxp  9349  eldju2ndl  9352  eldju2ndr  9353  djuun  9354  iscard3  9518  kmlem2  9576  ssfin4  9731  dffin7-2  9819  fin1a2lem11  9831  fin1a2lem12  9832  cfpwsdom  10005  elgch  10043  fpwwe2lem13  10063  canthp1lem2  10074  gch2  10096  elnn0  11898  un0addcl  11929  un0mulcl  11930  elxnn0  11968  ltxr  12509  elxr  12510  xrsupexmnf  12697  xrinfmexpnf  12698  supxrun  12708  ixxun  12753  difreicc  12869  iccsplit  12870  fzsplit2  12931  elfzp1  12956  uzsplit  12978  elfzp12  12985  fzosplit  13069  fzouzsplit  13071  elfzonlteqm1  13112  elfzo0l  13126  fzosplitsni  13147  elfzr  13149  elfzlmr  13150  hashnn0pnf  13701  hashf1lem2  13813  hash2pwpr  13833  pr2pwpr  13836  ccatrn  13942  cats1un  14082  fsumsplit  15096  sumsplit  15122  fprodsplit  15319  rpnnen2lem12  15577  sumeven  15737  sumodd  15738  saddisjlem  15812  lcmfunsnlem1  15980  lcmfunsnlem2lem1  15981  lcmfunsnlem2lem2  15982  lcmfunsnlem2  15983  coprmprod  16004  coprmproddvdslem  16005  nnnn0modprm0  16142  prm23lt5  16150  vdwapun  16309  ramubcl  16353  basprssdmsets  16548  mreexmrid  16913  lubun  17732  smndex1basss  18069  smndex1mgm  18071  smndex1mndlem  18073  smndex1n0mnd  18076  symgextf1  18548  gsumzsplit  19046  gsumzunsnd  19075  gsumunsnfd  19076  dprddisj2  19160  dmdprdsplit2lem  19166  dmdprdsplit2  19167  dprdsplit  19169  mplcoe1  20245  mplcoe5  20248  evlslem4  20287  cnfldfunALT  20557  mdetunilem9  21228  maducoeval2  21248  madugsum  21251  clslp  21755  islpi  21756  restntr  21789  pnfnei  21827  mnfnei  21828  iunconn  22035  refun0  22122  xkoptsub  22261  ptunhmeo  22415  fbun  22447  filconn  22490  fixufil  22529  ufildr  22538  alexsubALTlem2  22655  alexsubALTlem3  22656  alexsubALTlem4  22657  tsmssplit  22759  xrtgioo  23413  reconnlem2  23434  iccpnfcnv  23547  iccpnfhmeo  23548  rrxcph  23994  rrxdstprj1  24011  mbfss  24246  mbfmax  24249  itg2splitlem  24348  itg2split  24349  iblss2  24405  itgsplit  24435  limcdif  24473  ellimc2  24474  limcmpt  24480  limcres  24483  limccnp  24488  limccnp2  24489  limcco  24490  rollelem  24585  dvivthlem1  24604  dvne0  24607  lhop  24612  degltlem1  24665  ply1rem  24756  fta1glem2  24759  plypf1  24801  plyaddlem1  24802  plymullem1  24803  plycj  24866  ofmulrt  24870  taylfval  24946  abelthlem2  25019  abelthlem3  25020  reasinsin  25473  scvxcvx  25562  ppinprm  25728  chtnprm  25730  dchrfi  25830  lgsdir2  25905  2lgslem3  25979  2lgsoddprmlem3  25989  usgrexmplef  27040  cffldtocusgr  27228  vtxdun  27262  eucrct2eupth  28023  shunssi  29144  atomli  30158  atoml2i  30159  rmoun  30257  rmounid  30258  elunsn  30272  nelun  30273  suppovss  30425  isoun  30436  fzsplit3  30516  eliccioo  30607  cycpmco2  30775  cyc3co2  30782  cycpmrn  30785  lindsun  31021  lbsdiflsp0  31022  ordtconnlem1  31167  xrge0iifcnv  31176  xrge0iifiso  31178  xrge0iifhom  31180  esumsplit  31312  esumpad2  31315  measvuni  31473  sxbrsigalem0  31529  bnj1138  32060  bnj1137  32267  subfacp1lem4  32430  subfacp1lem5  32431  kur14lem7  32459  satfvsucsuc  32612  satfrnmapom  32617  satf0op  32624  satf0n0  32625  sat1el2xp  32626  fmlafvel  32632  isfmlasuc  32635  fmlaomn0  32637  satfv1fvfmla1  32670  2goelgoanfmla1  32671  mrsubcv  32757  mclsax  32816  dftrpred3g  33072  frrlem12  33134  frrlem13  33135  nosepdmlem  33187  brcup  33400  refssfne  33706  bj-eltag  34289  bj-0eltag  34290  bj-sngltag  34295  bj-projun  34306  tan2h  34883  poimirlem2  34893  poimirlem8  34899  poimirlem18  34909  poimirlem21  34912  poimirlem22  34913  poimirlem23  34914  poimirlem24  34915  poimirlem25  34916  poimirlem27  34918  poimirlem29  34920  poimirlem31  34922  poimirlem32  34923  ftc1anclem1  34966  ftc1anclem5  34970  dvasin  34977  dvacos  34978  eqfnun  34996  smprngopr  35329  elpadd  36934  paddval0  36945  hdmaplem4  38909  mapdh9a  38924  lzunuz  39363  jm2.23  39591  unxpwdom3  39693  hbtlem5  39726  rp-fakeinunass  39879  frege133d  40108  frege83  40290  frege131  40338  frege133  40340  uneqsn  40371  clsk1indlem3  40391  ntrneixb  40443  ntrneix3  40445  ntrneix13  40447  radcnvrat  40644  bccbc  40675  undif3VD  41214  iunconnlem2  41267  fnchoice  41284  elunnel2  41294  limciccioolb  41900  limcicciooub  41916  icccncfext  42168  cncfiooicclem1  42174  fourierdlem70  42460  fourierdlem80  42470  fourierdlem93  42483  fourierdlem101  42491  sge0split  42690  el1fzopredsuc  43524  iccpartltu  43584  iccpartgtl  43585  iccpartgt  43586  iccpartleu  43587  iccpartgel  43588  fmtno4prmfac  43733  31prm  43759  sbgoldbo  43951  nnsum4primeseven  43964  nnsum4primesevenALTV  43965  wtgoldbnnsum4prm  43966  bgoldbnnsum3prm  43968  bgoldbtbndlem3  43971  bgoldbtbnd  43973
  Copyright terms: Public domain W3C validator