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

Theorem elun 3737
 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 3202 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3202 . . 3 (𝐴𝐵𝐴 ∈ V)
3 elex 3202 . . 3 (𝐴𝐶𝐴 ∈ V)
42, 3jaoi 394 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
5 eleq1 2686 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 eleq1 2686 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
75, 6orbi12d 745 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
8 df-un 3565 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
97, 8elab2g 3341 . 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 3190   ∪ cun 3558 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 3192  df-un 3565 This theorem is referenced by:  elunnel1  3738  uneqri  3739  uncom  3741  uneq1  3744  unass  3754  ssun1  3760  unss1  3766  ssequn1  3767  unss  3771  rexun  3777  ralunb  3778  elsymdif  3833  symdif2  3836  indi  3855  undi  3856  unineq  3859  undif3  3870  undif3OLD  3871  rabun2  3888  reuun2  3892  undif4  4013  ssundif  4030  dfpr2  4173  elpwunsn  4202  eltpg  4205  pwpr  4405  pwtp  4406  uniun  4429  intun  4481  iinun2  4559  iunun  4577  iunxun  4578  iinuni  4582  brun  4673  pwunss  4989  pwssun  4990  opthprc  5137  xpundi  5142  xpundir  5143  difxp  5527  sossfld  5549  elsuci  5760  elsucg  5761  elsuc2g  5762  funun  5900  mptun  5992  unpreima  6307  suceloni  6975  ordsucun  6987  fnse  7254  reldmtpos  7320  dftpos4  7331  tpostpos  7332  wfrlem14  7388  wfrlem15  7389  oarec  7602  brdom2  7945  unxpdomlem3  8126  domunfican  8193  dfsup2  8310  wemapso2lem  8417  unwdomg  8449  unxpwdom2  8453  cantnfp1lem3  8537  rankunb  8673  iscard3  8876  kmlem2  8933  ssfin4  9092  dffin7-2  9180  fin1a2lem11  9192  fin1a2lem12  9193  cfpwsdom  9366  elgch  9404  fpwwe2lem13  9424  canthp1lem2  9435  gch2  9457  elnn0  11254  un0addcl  11286  un0mulcl  11287  elxnn0  11325  ltxr  11909  elxr  11910  xrsupexmnf  12094  xrinfmexpnf  12095  supxrun  12105  ixxun  12149  difreicc  12262  iccsplit  12263  fzsplit2  12324  elfzp1  12349  uzsplit  12369  elfzp12  12376  fzosplit  12458  fzouzsplit  12460  elfzonlteqm1  12500  elfzo0l  12515  fzosplitsni  12535  elfzr  12537  elfzlmr  12538  hashnn0pnf  13086  hashf1lem2  13194  hash2pwpr  13212  pr2pwpr  13215  ccatrn  13327  cats1un  13429  fsumsplit  14420  sumsplit  14446  fprodsplit  14640  rpnnen2lem12  14898  sumeven  15053  sumodd  15054  saddisjlem  15129  lcmfunsnlem1  15293  lcmfunsnlem2lem1  15294  lcmfunsnlem2lem2  15295  lcmfunsnlem2  15296  coprmprod  15318  coprmproddvdslem  15319  nnnn0modprm0  15454  prm23lt5  15462  vdwapun  15621  ramubcl  15665  basprssdmsets  15865  xpsfrnel2  16165  mreexmrid  16243  lubun  17063  symgextf1  17781  gsumzsplit  18267  gsumzunsnd  18295  gsumunsnfd  18296  dprddisj2  18378  dmdprdsplit2lem  18384  dmdprdsplit2  18385  dprdsplit  18387  mplcoe1  19405  mplcoe5  19408  evlslem4  19448  cnfldfunALT  19699  mdetunilem9  20366  maducoeval2  20386  madugsum  20389  clslp  20892  islpi  20893  restntr  20926  pnfnei  20964  mnfnei  20965  iunconn  21171  refun0  21258  xkoptsub  21397  ptunhmeo  21551  fbun  21584  filconn  21627  fixufil  21666  ufildr  21675  alexsubALTlem2  21792  alexsubALTlem3  21793  alexsubALTlem4  21794  tsmssplit  21895  xrtgioo  22549  reconnlem2  22570  iccpnfcnv  22683  iccpnfhmeo  22684  rrxcph  23120  rrxdstprj1  23132  mbfss  23353  mbfmax  23356  itg2splitlem  23455  itg2split  23456  iblss2  23512  itgsplit  23542  limcdif  23580  ellimc2  23581  limcmpt  23587  limcres  23590  limccnp  23595  limccnp2  23596  limcco  23597  rollelem  23690  dvivthlem1  23709  dvne0  23712  lhop  23717  degltlem1  23770  ply1rem  23861  fta1glem2  23864  plypf1  23906  plyaddlem1  23907  plymullem1  23908  plycj  23971  ofmulrt  23975  taylfval  24051  abelthlem2  24124  abelthlem3  24125  reasinsin  24557  scvxcvx  24646  ppinprm  24812  chtnprm  24814  dchrfi  24914  lgsdir2  24989  2lgslem3  25063  2lgsoddprmlem3  25073  usgrexmplef  26078  cffldtocusgr  26264  vtxdun  26297  eucrct2eupth  27005  shunssi  28115  atomli  29129  atoml2i  29130  isoun  29363  fzsplit3  29436  eliccioo  29466  ordtconnlem1  29794  xrge0iifcnv  29803  xrge0iifiso  29805  xrge0iifhom  29807  esumsplit  29938  esumpad2  29941  measvuni  30100  sxbrsigalem0  30156  bnj1138  30620  bnj1137  30824  subfacp1lem4  30926  subfacp1lem5  30927  kur14lem7  30955  mrsubcv  31168  mclsax  31227  dftrpred3g  31487  nosepdmlem  31620  brcup  31741  refssfne  32048  bj-eltag  32665  bj-0eltag  32666  bj-sngltag  32671  bj-projun  32682  tan2h  33072  poimirlem2  33082  poimirlem8  33088  poimirlem18  33098  poimirlem21  33101  poimirlem22  33102  poimirlem23  33103  poimirlem24  33104  poimirlem25  33105  poimirlem27  33107  poimirlem29  33109  poimirlem31  33111  poimirlem32  33112  ftc1anclem1  33156  ftc1anclem5  33160  dvasin  33167  dvacos  33168  eqfnun  33187  smprngopr  33522  elpadd  34604  paddval0  34615  hdmaplem4  36582  mapdh9a  36598  lzunuz  36850  jm2.23  37082  unxpwdom3  37184  hbtlem5  37218  rp-fakeinunass  37381  frege133d  37577  frege83  37761  frege131  37809  frege133  37811  uneqsn  37842  clsk1indlem3  37862  ntrneixb  37914  ntrneix3  37916  ntrneix13  37918  radcnvrat  38034  bccbc  38065  undif3VD  38640  iunconnlem2  38693  fnchoice  38710  elunnel2  38720  unima  38855  limciccioolb  39289  limcicciooub  39305  icccncfext  39435  cncfiooicclem1  39441  fourierdlem70  39730  fourierdlem80  39740  fourierdlem93  39753  fourierdlem101  39761  sge0split  39963  el1fzopredsuc  40662  iccpartltu  40689  iccpartgtl  40690  iccpartgt  40691  iccpartleu  40692  iccpartgel  40693  fmtno4prmfac  40813  31prm  40841  nnsum4primeseven  41007  nnsum4primesevenALTV  41008  wtgoldbnnsum4prm  41009  bgoldbnnsum3prm  41011  bgoldbtbndlem3  41014  bgoldbtbnd  41016
 Copyright terms: Public domain W3C validator