Theorem eliun 2624

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 1864	. 2 |- (A e. U_x e. B C -> A e. V)
2		elisset 1864	. . . 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 1790	. 2 |- (E.x e. B A e. C -> A e. V)
5		eleq1 1581	. . . 4 |- (y = A -> (y e. C <-> A e. C))
6	5	rexbidv 1711	. . 3 |- (y = A -> (E.x e. B y e. C <-> E.x e. B A e. C))
7		df-iun 2622	. . 3 |- U_x e. B C = {y | E.x e. B y e. C}
8	6, 7	elab2g 1947	. 2 |- (A e. V -> (A e. U_x e. B C <-> E.x e. B A e. C))
9	1, 4, 8	pm5.21nii 691	1 |- (A e. U_x e. B C <-> E.x e. B A e. C)

Syntax hints:   -> wi 3   <-> wb 153   = wceq 997   e. wcel 999  E.wrex 1693  Vcvv 1858  U_ciun 2620

This theorem is referenced by:  iunconst 2626  iuniin 2627  ss2iun 2631  iunss 2645  ssiun 2646  ssiun2 2647  iunrab 2650  iunid 2657  iun0 2658  0iun 2659  iunn0 2662  iunin2 2663  iundif2 2665  iindif2 2666  iunxsn 2667  iunxun 2669  iununi 2671  iunpwss 2673  iunpw 2971  cnvuni 3358  dmuni 3376  rnuni 3516  imaiun 3921  eluniima 3924  oalimcl 4252  oaass 4253  omordlim 4266  omlimcl 4267  oeordi 4272  trcl 4707  r1tr 4716  r1ord 4717  jech9.3 4728  rankr1 4736  r1pwcl 4749  cardaleph 4950  infxpidmlem6 7649  infxpidmlem7 7650  cncnplem2 7860  ubthlem5 8617

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-rex 1697  df-v 1859  df-iun 2622

Copyright terms: Public domain