Theorem iuneq2dv 4946

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

Hypothesis

Ref	Expression
iuneq2dv.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
iuneq2dv	⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem iuneq2dv

Step	Hyp	Ref	Expression
1		iuneq2dv.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
2	1	ralrimiva 3131	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)
3		iuneq2 4941	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
4	2, 3	syl 17	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-v 3433  df-ss 3900  df-iun 4923

This theorem is referenced by:  iuneq12dOLD  4950  iuneq12d  4951  iuneq2d  4952  fparlem3  8053  fparlem4  8054  oalim  8457  omlim  8458  oelim  8459  oelim2  8521  r1val3  9753  imasdsval  17470  acsfn  17616  tgidm  22963  cmpsub  23383  alexsublem  24027  bcth3  25316  ovoliunlem1  25487  voliunlem1  25535  uniiccdif  25563  uniioombllem2  25568  uniioombllem3a  25569  uniioombllem4  25571  itg2monolem1  25735  taylpfval  26348  dmdju  32739  ofpreima2  32758  fnpreimac  32762  ssdifidllem  33539  esum2dlem  34276  eulerpartlemgu  34561  cvmscld  35501  satom  35584  msubvrs  35788  mblfinlem2  38025  ftc1anclem6  38065  heibor  38188  prjspval2  43063  trclfvcom  44167  scottrankd  44692  meaiininclem  46929  carageniuncllem2  46965  hoidmv1le  47037  hoidmvle  47043  ovnhoilem2  47045  ovnhoi  47046  ovnlecvr2  47053  ovncvr2  47054  hspmbl  47072  ovolval4lem1  47092  ovnovollem1  47099  ovnovollem2  47100  iunhoiioo  47119  vonioolem2  47124  smflimlem4  47217  smflimlem6  47219