Theorem unieqd 2516

Description: Deduction of equality of two class unions.

Hypothesis

Ref	Expression
unieqd.1	⊢ (φ → A = B)

Assertion

Ref	Expression
unieqd	⊢ (φ → ∪A = ∪B)

Proof of Theorem unieqd

Step	Hyp	Ref	Expression
1		unieqd.1	. 2 ⊢ (φ → A = B)
2		unieq 2514	. 2 ⊢ (A = B → ∪A = ∪B)
3	1, 2	syl 10	1 ⊢ (φ → ∪A = ∪B)

Syntax hints:   → wi 3   = wceq 958  ∪cuni 2507

This theorem is referenced by:  uniprg 2520  unisng 2522  unisn2 2881  unisn3 2882  ordunisuc 3095  orduniss2 3096  elxp4 3459  elxp5 3460  fvprc 3727  fveq1 3729  fveq2 3730  fvres 3740  funfv 3776  funfv2 3777  fvopabn 3792  fvopab5 3799  fniunfv 3871  tz7.44-3 3936  rdgeq1 3940  rdgeq2 3941  rdglem2 3944  rdglimt 3954  rdglim2 3955  1stval 4087  2ndval 4088  fo1st 4097  fo2nd 4098  f1stres 4099  f2ndres 4100  1st2val 4101  2nd2val 4102  oaabs 4258  xpcomen 4445  xpassen 4447  xpdom2 4448  xpmapenlem2 4503  xpmapenlem4 4505  xpmapenlem5 4506  mapunen 4508  unifiOLD 4570  supeq1 4584  rankuni 4708  aceq6a 4751  kmlem9 4783  kmlem11 4785  kmlem12 4786  zorn2lem1 4798  zorn2 4806  subvalt 5369  divval 5716  dfinfmr 6069  infmsup 6070  supxrre 6085  flvalt 6227  revalt 6756  imvalt 6757  sumeq1 6982  sumeq2 6985  dffsum 6998  dfisum 7191  isumvalt 7192  isumnul 7203  acdc3lem 7487  acdc3 7488  acdc2lem1 7489  acdc2 7491  acdc5lem1 7492  acdc5 7494  acdclem 7495  acdc 7496  xpnnen 7500  isbasisg 7610  basis1t 7613  tgvalt 7615  eltgt 7617  ntrfval 7664  ntrval 7673  cncnplem4 7774  bcth 8029  grpidval 8054  grpinvfval 8062  grpinvval 8063  addinv 8124  isps 8641  spwval2 8649  spwval 8655  spwpr4OLD 8658  spwpr4aOLD 8659  pjmvalt 9233  pjvalt 9234  adjvalt 9809  adjval2t 9810  cnlnadjlem4 9998  nmopadjle 10016  cdj3lem2 10357

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-uni 2508

Copyright terms: Public domain