Theorem elun 3274

Description: Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.)

Assertion

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

Proof of Theorem elun

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2746	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2746	. . 3 |- ( A e. B -> A e. _V )
3		elex 2746	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 716	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2238	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2238	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 793	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3131	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2882	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 704	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 105   \/ wo 708   = wceq 1353   e. wcel 2146   _Vcvv 2735   u. cun 3125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-un 3131

This theorem is referenced by:  uneqri  3275  uncom  3277  uneq1  3280  unass  3290  ssun1  3296  unss1  3302  ssequn1  3303  unss  3307  rexun  3313  ralunb  3314  unssdif  3368  unssin  3372  inssun  3373  indi  3380  undi  3381  difundi  3385  difindiss  3387  undif3ss  3394  symdifxor  3399  rabun2  3412  reuun2  3416  undif4  3483  ssundifim  3504  dcun  3531  dfpr2  3608  eltpg  3634  pwprss  3801  pwtpss  3802  uniun  3824  intun  3871  iunun  3960  iunxun  3961  iinuniss  3964  brun  4049  undifexmid  4188  exmidundif  4201  exmidundifim  4202  pwunss  4277  elsuci  4397  elsucg  4398  elsuc2g  4399  ordsucim  4493  sucprcreg  4542  opthprc  4671  xpundi  4676  xpundir  4677  funun  5252  mptun  5339  unpreima  5633  reldmtpos  6244  dftpos4  6254  tpostpos  6255  onunsnss  6906  unfidisj  6911  undifdcss  6912  fidcenumlemrks  6942  djulclb  7044  eldju  7057  eldju2ndl  7061  eldju2ndr  7062  ctssdccl  7100  pw1nel3  7220  sucpw1nel3  7222  elnn0  9149  un0addcl  9180  un0mulcl  9181  elxnn0  9212  ltxr  9744  elxr  9745  fzsplit2  10018  elfzp1  10040  uzsplit  10060  elfzp12  10067  fz01or  10079  fzosplit  10145  fzouzsplit  10147  elfzonlteqm1  10178  fzosplitsni  10203  hashinfuni  10723  hashennnuni  10725  hashunlem  10750  zfz1isolemiso  10785  summodclem3  11354  fsumsplit  11381  fsumsplitsn  11384  sumsplitdc  11406  fprodsplitdc  11570  fprodsplit  11571  fprodunsn  11578  fprodsplitsn  11607  nnnn0modprm0  12220  prm23lt5  12228  reopnap  13589  lgsdir2  13985  djulclALT  14093  djurclALT  14094  bj-charfun  14099  bj-nntrans  14243  bj-nnelirr  14245  exmid1stab  14290