Theorem iuneq1d 4988

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

Syntax hints:   → wi 4   = wceq 1567  ∪ ciun 4960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-v 3465  df-ss 3930  df-iun 4962

This theorem is referenced by:  iuneq12dOLD  4989  disjxiun  5110  kmlem11  10143  indval2  12222  prmreclem4  16978  imasval  17564  iundisj  25675  iundisj2  25676  voliunlem1  25677  iunmbl  25680  volsup  25683  uniioombllem4  25713  iuninc  32845  iundisjf  32874  iundisj2f  32875  suppovss  32966  iundisjfi  33081  iundisj2fi  33082  iundisjcnt  33083  sigaclcu3  34456  fiunelros  34508  meascnbl  34553  bnj1113  35118  bnj155  35211  bnj570  35237  bnj893  35260  cvmliftlem10  35684  mrsubvrs  35912  msubvrs  35950  voliunnfl  38202  volsupnfl  38203  heiborlem3  38351  heibor  38359  iunrelexp0  44319  iunp1  45677  iundjiunlem  47064  iundjiun  47065  meaiuninclem  47085  meaiuninc  47086  carageniuncllem1  47126  carageniuncllem2  47127  carageniuncl  47128  caratheodorylem1  47131  caratheodorylem2  47132  imasubclem3  49768  imaf1hom  49770