Theorem iuneq2dv 4542

Description: Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.)

Hypothesis

Ref	Expression
iuneq2dv.1	|- ( ( ph /\ x e. A ) -> B = C )

Assertion

Ref	Expression
iuneq2dv	|- ( ph -> U_ x e. A B = U_ x e. A C )

Distinct variable group:   ph, x

Allowed substitution hints:   A( x)   B( x)   C( x)

Proof of Theorem iuneq2dv

Step	Hyp	Ref	Expression
1		iuneq2dv.1	. . 3 |- ( ( ph /\ x e. A ) -> B = C )
2	1	ralrimiva 2966	. 2 |- ( ph -> A. x e. A B = C )
3		iuneq2 4537	. 2 |- ( A. x e. A B = C -> U_ x e. A B = U_ x e. A C )
4	2, 3	syl 17	1 |- ( ph -> U_ x e. A B = U_ x e. A C )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   U_ciun 4520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-iun 4522

This theorem is referenced by:  iuneq12d  4546  iuneq2d  4547  fparlem3  7279  fparlem4  7280  oalim  7612  omlim  7613  oelim  7614  oelim2  7675  r1val3  8701  imasdsval  16175  acsfn  16320  tgidm  20784  cmpsub  21203  alexsublem  21848  bcth3  23128  ovoliunlem1  23270  voliunlem1  23318  uniiccdif  23346  uniioombllem2  23351  uniioombllem3a  23352  uniioombllem4  23354  itg2monolem1  23517  taylpfval  24119  ofpreima2  29466  esum2dlem  30154  eulerpartlemgu  30439  cvmscld  31255  msubvrs  31457  mblfinlem2  33447  ftc1anclem6  33490  heibor  33620  trclfvcom  38015  meaiininclem  40700  carageniuncllem2  40736  hoidmv1le  40808  hoidmvle  40814  ovnhoilem2  40816  ovnhoi  40817  ovnlecvr2  40824  ovncvr2  40825  hspmbl  40843  ovolval4lem1  40863  ovnovollem1  40870  ovnovollem2  40871  iunhoiioo  40890  vonioolem2  40895  smflimlem4  40982  smflimlem6  40984