Theorem iuneq1d 4949

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

Syntax hints:   → wi 4   = wceq 1547  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rex 3064  df-v 3433  df-ss 3900  df-iun 4923

This theorem is referenced by:  iuneq12dOLD  4950  disjxiun  5069  kmlem11  10074  indval2  12155  prmreclem4  16881  imasval  17466  iundisj  25533  iundisj2  25534  voliunlem1  25535  iunmbl  25538  volsup  25541  uniioombllem4  25571  iuninc  32649  iundisjf  32678  iundisj2f  32679  suppovss  32773  iundisjfi  32888  iundisj2fi  32889  iundisjcnt  32890  sigaclcu3  34306  fiunelros  34358  meascnbl  34403  bnj1113  34968  bnj155  35061  bnj570  35087  bnj893  35110  cvmliftlem10  35522  mrsubvrs  35750  msubvrs  35788  voliunnfl  38031  volsupnfl  38032  heiborlem3  38180  heibor  38188  iunrelexp0  44146  iunp1  45514  iundjiunlem  46902  iundjiun  46903  meaiuninclem  46923  meaiuninc  46924  carageniuncllem1  46964  carageniuncllem2  46965  carageniuncl  46966  caratheodorylem1  46969  caratheodorylem2  46970  imasubclem3  49596  imaf1hom  49598