Theorem iuneq1d 4951

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

Hypothesis

Ref	Expression
iuneq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

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

Proof of Theorem iuneq1d

Step	Hyp	Ref	Expression
1		iuneq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		iuneq1 4940	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   = wceq 1539  ∪ ciun 4924

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 3434  df-in 3894  df-ss 3904  df-iun 4926

This theorem is referenced by:  iuneq12d  4952  disjxiun  5071  kmlem11  9916  prmreclem4  16620  imasval  17222  iundisj  24712  iundisj2  24713  voliunlem1  24714  iunmbl  24717  volsup  24720  uniioombllem4  24750  iuninc  30900  iundisjf  30928  iundisj2f  30929  suppovss  31017  iundisjfi  31117  iundisj2fi  31118  iundisjcnt  31119  indval2  31982  sigaclcu3  32090  fiunelros  32142  meascnbl  32187  bnj1113  32765  bnj155  32859  bnj570  32885  bnj893  32908  cvmliftlem10  33256  mrsubvrs  33484  msubvrs  33522  voliunnfl  35821  volsupnfl  35822  heiborlem3  35971  heibor  35979  iunrelexp0  41310  iunp1  42614  iundjiunlem  43997  iundjiun  43998  meaiuninclem  44018  meaiuninc  44019  carageniuncllem1  44059  carageniuncllem2  44060  carageniuncl  44061  caratheodorylem1  44064  caratheodorylem2  44065