Theorem unieqd 3188

Description: Deduction of equality of two class unions.

Hypothesis

Ref	Expression
unieqd.1	|- (ph -> A = B)

Assertion

Ref	Expression
unieqd	|- (ph -> U.A = U.B)

Proof of Theorem unieqd

Step	Hyp	Ref	Expression
1		unieqd.1	. 2 |- (ph -> A = B)
2		unieq 3185	. 2 |- (A = B -> U.A = U.B)
3	1, 2	syl 12	1 |- (ph -> U.A = U.B)

Syntax hints:   -> wi 3   = wceq 1298  U.cuni 3177

This theorem is referenced by:  uniprg 3192  unisng 3194  unisn2 3799  unisn3 3800  ordunisuc 3911  ordunisucOLD 3912  orduniss2 3913  onsucuni2 3914  elxp4 4379  elxp5 4380  fvprc 4678  fveq1 4680  fveq2 4681  fvres 4691  funfv 4731  funfv2 4732  dffv2 4734  fvopabn 4749  fvopab5 4756  fvopab6 4757  fniunfv 4841  1stval 5022  2ndval 5023  fo1st 5032  fo2nd 5033  f1stres 5034  f2ndres 5035  1st2val 5038  2nd2val 5039  iotaeq 5093  iotabi 5094  uniabio 5095  iotanul 5098  onopriun 5118  tz7.44-3 5138  rdgeq1 5142  rdgeq2 5143  rdglem2 5146  rdglim 5156  rdglim2 5157  oaabs 5309  xpcomen 5498  xpassen 5500  xpdom2 5501  xpmapenlem2 5591  xpmapenlem4 5593  xpmapenlem5 5594  mapunen 5596  unifi 5648  supeq1 5665  ordtypelem1 5684  ordtypelem6 5689  ordtype 5691  hartog 5693  rankuni 5809  aceq6a 5903  kmlem9 5935  kmlem11 5937  kmlem12 5938  zorn2lem1 5950  zorn2 5958  dfinfmr 7276  infmsup 7277  supxrre 7292  flval 7464  reval 8005  imval 8006  sumeq1 8242  sumeq2 8245  dffsum 8258  dfisum 8452  isumval 8453  isumnul 8464  acdc3lem 8754  acdc3 8755  acdc2lem1 8757  acdc2 8759  acdc5lem1 8760  acdc5 8762  acdclem 8763  acdc 8764  xpnnen 8768  isbasisg 8880  basis1 8883  tgval 8886  eltg 8888  txuni 8935  ntrfval 8943  ntrval 8952  cncnplem4 9054  bcth 9310  gid0 9338  grpidvallem 9341  grpidval 9342  grpinvfval 9350  grpinvval 9351  addinv 9436  ajval 9863  isps 9988  spwval2 9996  spwval 10002  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  istoset 10209  fmbas 10311  isdir 10352  idrval 10374  pjmval 10871  pjval 10872  adjval 11451  adjval2 11452  cnlnadjlem4 11640  nmopadjlei 11658  cdj3lem2 12007  trcleq1 13926  trcleq2 13927  trcleq3 13928  fldsqcp2 14378  valfunun 14460  repfuntw 14502  isprs 14565  ubos2 14598  ubos 14599  supdef 14604  mxlelt2 14606  mxlelt 14607  mnlelt2 14608  isdir2 14640  rngunval2 14774  usptoplem 14917  istopx 14918  prtoptop 14919  usptop 14920  invtrgrp 14979  supexr 15043  dualalg 15131  vtarl 15264  ordtypelem1OLD 15375  ordtypelem6OLD 15380  ordtypeOLD 15382  hartogOLD 15384  compfipin0lem 15435  compfipin0 15436  alexsublem3 15439  isfne 15480  neibastop2lem1 15519  neibastop2lem4 15522  topmtcl 15525  tailf 15633  supeq2 15760  heiborlem8 15962  heiborlem11 15965

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-rex 2110  df-uni 3178

Copyright terms: Public domain