Theorem unieqi 3902

Description: Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
unieqi.1	⊢ A = B

Assertion

Ref	Expression
unieqi	⊢ ∪A = ∪B

Proof of Theorem unieqi

Step	Hyp	Ref	Expression
1		unieqi.1	. 2 ⊢ A = B
2		unieq 3901	. 2 ⊢ (A = B → ∪A = ∪B)
3	1, 2	ax-mp 5	1 ⊢ ∪A = ∪B

Syntax hints:   = wceq 1642  ∪cuni 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-rex 2621  df-uni 3893

This theorem is referenced by:  elunirab  3905  unisn  3908  iotajust  4339  dfiota2  4341  cbviota  4345  sb8iota  4347  dfiota4  4373  op1sta  5073  opswap  5075  op2nda  5077  funfv2  5377  funfv2f  5378  fvco2  5383  funiunfv  5468  elunirn  5471  uniqs  5985