Theorem unieqi 2515

Description: Inference of equality of two class unions.

Hypothesis

Ref	Expression
unieqi.1	|- A = B

Assertion

Ref	Expression
unieqi	|- U.A = U.B

Proof of Theorem unieqi

Step	Hyp	Ref	Expression
1		unieqi.1	. 2 |- A = B
2		unieq 2514	. 2 |- (A = B -> U.A = U.B)
3	1, 2	ax-mp 7	1 |- U.A = U.B

Syntax hints:   = wceq 958  U.cuni 2507

This theorem is referenced by:  elunirab 2518  unisn 2521  unidif0 2744  uniop 2814  reuuni1 2888  reucl 2891  reuuni3 2892  reuunixfr 2912  univ 2915  unisuc 3052  op1sta 3454  op2nda 3458  fv2 3726  funfv2f 3778  funiunfv 3872  elunirn 3874  tfrlem9 3925  tz7.44-2 3935  tz7.44-3 3936  dfrdg2 3939  1st0 4089  2nd0 4090  unielxp 4113  ecqs 4303  xpassen 4447  supex 4586  unir1 4677  rankxplim2 4723  rankxplim3 4724  rankxpsuc 4725  hta 4738  aceq5lem2 4746  kmlem11 4785  infmsup 6070  cbvsum 6986  isumclimtf 7195  isumclt 7209  bastgt 7621  fctopOLD 7647  cctop 7649  spwval2 8649  cnlnadjlem5 9999  cnlnadj 10004  adjbdlnt 10011  nmopadjle 10016  cdj3lem3 10360  cdj3lem3b 10362  stoi 10610

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