Theorem unieqd 1929

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 1927	. 2 |- (A = B -> U.A = U.B)
3	1, 2	syl 12	1 |- (ph -> U.A = U.B)

Syntax hints:   -> wi 2   = wceq 1091  U.cuni 1919

This theorem is referenced by:  unisng 1933  supeq1 2155  ordunisuc 2339  elxp4 2640  elxp5 2641  fvprc 2829  fveq1 2831  fveq2 2832  fvres 2840  fniunfv 2860  funfv 2862  funfv2 2863  fvopabn 2873  tz7.44-3 2968  rdgeq1 2972  rdgeq2 2973  rdglem2 2976  rdglimt 2986  rdglim2 2987  1stval 3089  2ndval 3090  fo1st 3094  fo2nd 3095  f1stres 3096  1st2val 3097  xpcomen 3343  xpassen 3344  xpdom2 3345  xpmapenlem2 3392  xpmapenlem4 3394  xpmapenlem5 3395  mapunen 3397  aceq6a 3564  kmlem8 3587  kmlem10 3589  kmlem11 3590  zornlem1 3603  zorn 3611  subval 4134  divval 4217  flvalt 4623  revalt 4794  imvalt 4795  xpnnen 4927  pjmvalt 5245  pjvalt 5246

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-uni 1920

metamath.org