Theorem eliun 2567

Description: Membership in indexed union.

Assertion

Ref	Expression
eliun	|- (A e. U_x e. B C <-> E.x e. B A e. C)

Distinct variable group:   x,A

Proof of Theorem eliun

Step	Hyp	Ref	Expression
1		elisset 1815	. 2 |- (A e. U_x e. B C -> A e. V)
2		elisset 1815	. . . 4 |- (A e. C -> A e. V)
3	2	a1i 8	. . 3 |- (x e. B -> (A e. C -> A e. V))
4	3	r19.23aiv 1742	. 2 |- (E.x e. B A e. C -> A e. V)
5		eleq1 1533	. . . 4 |- (y = A -> (y e. C <-> A e. C))
6	5	rexbidv 1663	. . 3 |- (y = A -> (E.x e. B y e. C <-> E.x e. B A e. C))
7		df-iun 2565	. . 3 |- U_x e. B C = {y | E.x e. B y e. C}
8	6, 7	elab2g 1898	. 2 |- (A e. V -> (A e. U_x e. B C <-> E.x e. B A e. C))
9	1, 4, 8	pm5.21nii 678	1 |- (A e. U_x e. B C <-> E.x e. B A e. C)

Syntax hints:   -> wi 3   <-> wb 146   = wceq 955   e. wcel 957  E.wrex 1645  Vcvv 1809  U_ciun 2563

This theorem is referenced by:  iunconst 2569  iuniin 2570  ss2iun 2574  iunss 2588  ssiun 2589  ssiun2 2590  iunrab 2593  iunid 2600  iun0 2601  0iun 2602  iunn0 2604  iunin2 2605  iundif2 2607  iindif2 2608  iunxsn 2609  iunxun 2611  iununi 2613  iunpwss 2615  iunpw 2911  cnvuni 3298  dmuni 3316  rnuni 3456  imaiun 3861  eluniima 3864  oalimcl 4191  oaass 4192  omordlim 4205  omlimcl 4206  oeordi 4211  trcl 4632  r1tr 4641  r1ord 4642  jech9.3 4653  rankr1 4661  r1pwcl 4674  cardaleph 4872  infxpidmlem6 7536  infxpidmlem7 7537  cncnplem2 7754  ubthlem5 8517

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-rex 1649  df-v 1810  df-iun 2565

Copyright terms: Public domain