Theorem iuneq2dv 4676

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

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631   ∈ wcel 2145  ∀wral 3061  ∪ ciun 4654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-v 3353  df-in 3730  df-ss 3737  df-iun 4656

This theorem is referenced by:  iuneq12d  4680  iuneq2d  4681  fparlem3  7429  fparlem4  7430  oalim  7765  omlim  7766  oelim  7767  oelim2  7828  r1val3  8864  imasdsval  16382  acsfn  16526  tgidm  21004  cmpsub  21423  alexsublem  22067  bcth3  23346  ovoliunlem1  23489  voliunlem1  23537  uniiccdif  23565  uniioombllem2  23570  uniioombllem3a  23571  uniioombllem4  23573  itg2monolem1  23736  taylpfval  24338  ofpreima2  29803  esum2dlem  30491  eulerpartlemgu  30776  cvmscld  31590  msubvrs  31792  mblfinlem2  33776  ftc1anclem6  33818  heibor  33948  trclfvcom  38537  meaiininclem  41216  carageniuncllem2  41252  hoidmv1le  41324  hoidmvle  41330  ovnhoilem2  41332  ovnhoi  41333  ovnlecvr2  41340  ovncvr2  41341  hspmbl  41359  ovolval4lem1  41379  ovnovollem1  41386  ovnovollem2  41387  iunhoiioo  41406  vonioolem2  41411  smflimlem4  41498  smflimlem6  41500