Theorem iuneq1d 4977

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

Syntax hints:   → wi 4   = wceq 1560  ∪ ciun 4949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3087  df-v 3456  df-ss 3921  df-iun 4951

This theorem is referenced by:  iuneq12dOLD  4978  disjxiun  5097  kmlem11  10117  indval2  12200  prmreclem4  16955  imasval  17541  iundisj  25607  iundisj2  25608  voliunlem1  25609  iunmbl  25612  volsup  25615  uniioombllem4  25645  iuninc  32757  iundisjf  32786  iundisj2f  32787  suppovss  32880  iundisjfi  32995  iundisj2fi  32996  iundisjcnt  32997  sigaclcu3  34416  fiunelros  34468  meascnbl  34513  bnj1113  35078  bnj155  35171  bnj570  35197  bnj893  35220  cvmliftlem10  35641  mrsubvrs  35869  msubvrs  35907  voliunnfl  38160  volsupnfl  38161  heiborlem3  38309  heibor  38317  iunrelexp0  44275  iunp1  45643  iundjiunlem  47030  iundjiun  47031  meaiuninclem  47051  meaiuninc  47052  carageniuncllem1  47092  carageniuncllem2  47093  carageniuncl  47094  caratheodorylem1  47097  caratheodorylem2  47098  imasubclem3  49724  imaf1hom  49726