Theorem iuneq2d 4547

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

Hypothesis

Ref	Expression
iuneq2d.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝑥,𝐴

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

Proof of Theorem iuneq2d

Step	Hyp	Ref	Expression
1		iuneq2d.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
2	1	adantr 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	iuneq2dv 4542	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990  ∪ 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:  iununi  4610  oelim2  7675  ituniiun  9244  dfrtrclrec2  13797  rtrclreclem1  13798  rtrclreclem2  13799  rtrclreclem4  13801  imasval  16171  mreacs  16319  cnextval  21865  taylfval  24113  iunpreima  29383  reprdifc  30705  msubvrs  31457  trpredeq1  31720  trpredeq2  31721  neibastop2  32356  voliunnfl  33453  sstotbnd2  33573  equivtotbnd  33577  totbndbnd  33588  heiborlem3  33612  eliunov2  37971  fvmptiunrelexplb0d  37976  fvmptiunrelexplb1d  37978  comptiunov2i  37998  trclrelexplem  38003  dftrcl3  38012  trclfvcom  38015  cnvtrclfv  38016  cotrcltrcl  38017  trclimalb2  38018  trclfvdecomr  38020  dfrtrcl3  38025  dfrtrcl4  38030  isomenndlem  40744  ovnval  40755  hoicvr  40762  hoicvrrex  40770  ovnlecvr  40772  ovncvrrp  40778  ovnsubaddlem1  40784  hoidmvlelem3  40811  hoidmvle  40814  ovnhoilem1  40815  ovnovollem1  40870  smflimlem3  40981  otiunsndisjX  41298