Theorem unieqd 3820

Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)

Hypothesis

Ref	Expression
unieqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
unieqd	⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)

Proof of Theorem unieqd

Step	Hyp	Ref	Expression
1		unieqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		unieq 3818	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1353  ∪ cuni 3809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3810

This theorem is referenced by:  uniprg  3824  unisng  3826  unisn3  4445  onsucuni2  4563  opswapg  5115  elxp4  5116  elxp5  5117  iotaeq  5186  iotabi  5187  uniabio  5188  funfvdm  5579  funfvdm2  5580  fvun1  5582  fniunfv  5762  funiunfvdm  5763  1stvalg  6142  2ndvalg  6143  fo1st  6157  fo2nd  6158  f1stres  6159  f2ndres  6160  2nd1st  6180  cnvf1olem  6224  brtpos2  6251  dftpos4  6263  tpostpos  6264  recseq  6306  tfrexlem  6334  ixpsnf1o  6735  xpcomco  6825  xpassen  6829  xpdom2  6830  supeq1  6984  supeq2  6987  supeq3  6988  supeq123d  6989  en2other2  7194  dfinfre  8912  hashinfom  10757  hashennn  10759  fsumcnv  11444  fprodcnv  11632  tgval  12710  ptex  12712  isbasisg  13514  basis1  13517  baspartn  13520  eltg  13522  ntrfval  13570  ntrval  13580  tgrest  13639  restuni2  13647  lmfval  13662  cnfval  13664  cnpfval  13665  txtopon  13732  txswaphmeolem  13790  peano4nninf  14725