Theorem iuneq2dv 4949

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 3113	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)
3		iuneq2 4944	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
4	2, 3	syl 17	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ∪ ciun 4925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3432  df-in 3894  df-ss 3904  df-iun 4927

This theorem is referenced by:  iuneq12d  4953  iuneq2d  4954  fparlem3  7942  fparlem4  7943  oalim  8350  omlim  8351  oelim  8352  oelim2  8414  r1val3  9584  imasdsval  17214  acsfn  17356  tgidm  22118  cmpsub  22539  alexsublem  23183  bcth3  24483  ovoliunlem1  24654  voliunlem1  24702  uniiccdif  24730  uniioombllem2  24735  uniioombllem3a  24736  uniioombllem4  24738  itg2monolem1  24903  taylpfval  25512  ofpreima2  30989  fnpreimac  30994  esum2dlem  32046  eulerpartlemgu  32330  cvmscld  33221  satom  33304  msubvrs  33508  mblfinlem2  35801  ftc1anclem6  35841  heibor  35965  prjspval2  40438  trclfvcom  41290  scottrankd  41825  meaiininclem  43983  carageniuncllem2  44019  hoidmv1le  44091  hoidmvle  44097  ovnhoilem2  44099  ovnhoi  44100  ovnlecvr2  44107  ovncvr2  44108  hspmbl  44126  ovolval4lem1  44146  ovnovollem1  44153  ovnovollem2  44154  iunhoiioo  44173  vonioolem2  44178  smflimlem4  44265  smflimlem6  44267