Theorem iuneq1d 4355

Description: Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)

Hypothesis

Ref	Expression
iuneq1d.1

Assertion

Ref	Expression
iuneq1d

Distinct variable groups:   ,   ,

Proof of Theorem iuneq1d

Step	Hyp	Ref	Expression
1		iuneq1d.1	. 2
2		iuneq1 4344	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  =wceq 1395  U_ciun 4330

This theorem is referenced by:  iuneq12d  4356  disjxiun  4449  kmlem11  8561  prmreclem4  14437  imasval  14908  iundisj  21958  iundisj2  21959  voliunlem1  21960  iunmbl  21963  volsup  21966  uniioombllem4  21995  iuninc  27428  iundisjf  27448  iundisj2f  27449  iundisjfi  27601  iundisj2fi  27602  iundisjcnt  27603  indval2  28028  sigaclcu3  28122  meascnbl  28190  cvmliftlem10  28739  mrsubvrs  28882  msubvrs  28920  voliunnfl  30058  volsupnfl  30059  heiborlem3  30309  heibor  30317  bnj1113  33844  bnj155  33937  bnj570  33963  bnj893  33986

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-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-in 3482  df-ss 3489  df-iun 4332