Theorem iuneq1d 4545

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

Syntax hints:   → wi 4   = wceq 1483  ∪ 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:  iuneq12d  4546  disjxiun  4649  disjxiunOLD  4650  kmlem11  8982  prmreclem4  15623  imasval  16171  iundisj  23316  iundisj2  23317  voliunlem1  23318  iunmbl  23321  volsup  23324  uniioombllem4  23354  iuninc  29379  iundisjf  29402  iundisj2f  29403  iundisjfi  29555  iundisj2fi  29556  iundisjcnt  29557  indval2  30076  sigaclcu3  30185  fiunelros  30237  meascnbl  30282  bnj1113  30856  bnj155  30949  bnj570  30975  bnj893  30998  cvmliftlem10  31276  mrsubvrs  31419  msubvrs  31457  voliunnfl  33453  volsupnfl  33454  heiborlem3  33612  heibor  33620  iunrelexp0  37994  iunp1  39235  iundjiunlem  40676  iundjiun  40677  meaiuninclem  40697  meaiuninc  40698  carageniuncllem1  40735  carageniuncllem2  40736  carageniuncl  40737  caratheodorylem1  40740  caratheodorylem2  40741