Theorem elun 2225

Description: Expansion of membership in class union. Theorem 12 of [Suppes] p. 25.

Assertion

Ref	Expression
elun	|- (A e. (B u. C) <-> (A e. B \/ A e. C))

Proof of Theorem elun

Step	Hyp	Ref	Expression
1		elisset 1863	. 2 |- (A e. (B u. C) -> A e. V)
2		elisset 1863	. . 3 |- (A e. B -> A e. V)
3		elisset 1863	. . 3 |- (A e. C -> A e. V)
4	2, 3	jaoi 339	. 2 |- ((A e. B \/ A e. C) -> A e. V)
5		eleq1 1577	. . . 4 |- (x = A -> (x e. B <-> A e. B))
6		eleq1 1577	. . . 4 |- (x = A -> (x e. C <-> A e. C))
7	5, 6	orbi12d 630	. . 3 |- (x = A -> ((x e. B \/ x e. C) <-> (A e. B \/ A e. C)))
8		df-un 2102	. . 3 |- (B u. C) = {x | (x e. B \/ x e. C)}
9	7, 8	elab2g 1946	. 2 |- (A e. V -> (A e. (B u. C) <-> (A e. B \/ A e. C)))
10	1, 4, 9	pm5.21nii 683	1 |- (A e. (B u. C) <-> (A e. B \/ A e. C))

Syntax hints:   <-> wb 144   \/ wo 220   = wceq 992   e. wcel 994  Vcvv 1857   u. cun 2097

This theorem is referenced by:  uneqri 2226  uncom 2228  uneq1 2229  hbun 2238  unass 2239  ssun1 2245  unss1 2251  unss 2256  dfun2 2295  indi 2303  undi 2304  unineq 2307  symdif2 2318  unab 2319  reuun2 2330  undif4 2378  disjssun 2379  ssundif 2398  dfpr2 2480  eltp 2500  pwpr 2567  uniun 2586  intun 2629  iinun2 2678  iunun 2683  iunxun 2684  iinuni 2685  iununi 2686  brun 2735  pwunss 2904  pwssun 2905  pwundif 2906  elsuci 3039  elsucg 3040  elsuc2g 3041  sucid 3051  elpwunsn 3135  suceloni 3170  ordsucun 3180  opthprc 3306  xpundi 3310  xpundir 3311  dmun 3408  cnvun 3540  coundi 3600  coundir 3601  funun 3659  fopabap 3955  erref 4415  brdom2 4529  ac6sfilem3 4590  sucprcreg 4743  rankun 4837  kmlem2 4912  unxpdomlem 4993  iscard3 5038  pnfxr 5647  mnfxr 5648  ltxr 5649  elxr 5689  xrsupexmnf 6242  xrinfmexpnf 6243  supxrun 6253  elnn0 6269  icounlem 6539  snunioolem 6541  ioojoin 6543  fzsuc 6636  clslp 7958  islpi 7959  metelcls 8176  efif1lem5 9006  efif1lem7 9008  shunssi 9613  atomli 10591  atoml2i 10592  domrngref 10764  cdrci 10994  subntr 11482  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  reconn 11512  refssfne 11565  locfincomp 11575  comppfsc 11578  extbas1 11641  ufprim 11654  filssufillem 11655  filssufil 11656  filcon 11665  ufcondr 11666  cnpfillim 11686  elfilmap 11690  filnetlem1 11763  ralun 11789  unpreima 11794  difxp 11798  indexf 11847  iccsplit 11919  piececn 11955  heiborlem15 12025  phtpycolem5 12097  phtpyco 12098

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102

Copyright terms: Public domain