Theorem unieqi 3901

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 3900	. 2 ⊢ (A = B → ∪A = ∪B)
3	1, 2	ax-mp 5	1 ⊢ ∪A = ∪B

Syntax hints:   = wceq 1642  ∪cuni 3891

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 2478  df-rex 2620  df-uni 3892

This theorem is referenced by:  elunirab  3904  unisn  3907  iotajust  4338  dfiota2  4340  cbviota  4344  sb8iota  4346  dfiota4  4372  op1sta  5072  opswap  5074  op2nda  5076  funfv2  5376  funfv2f  5377  fvco2  5382  funiunfv  5467  elunirn  5470  uniqs  5984