Theorem dfiun2 4364

Description: Alternate definition of indexed union when is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 27-Jun-1998.) (Revised by David Abernethy, 19-Jun-2012.)

Hypothesis

Ref	Expression
dfiun2.1

Assertion

Ref	Expression
dfiun2

Distinct variable groups:   ,   ,   ,

Proof of Theorem dfiun2

Step	Hyp	Ref	Expression
1		dfiun2g 4362	. 2
2		dfiun2.1	. . 3
3	2	a1i 11	. 2
4	1, 3	mprg 2820	1

Syntax hints:  =wceq 1395  e.wcel 1818  {cab 2442  E.wrex 2808  cvv 3109  U.cuni 4249  U_ciun 4330

This theorem is referenced by:  fniunfv  6159  funcnvuni  6753  fun11iun  6760  tfrlem8  7072  rdglim2a  7118  rankuni  8302  cardiun  8384  kmlem11  8561  cfslb2n  8669  enfin2i  8722  pwcfsdom  8979  rankcf  9176  tskuni  9182  discmp  19898  cmpsublem  19899  cmpsub  19900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-uni 4250  df-iun 4332