Theorem unieqi 2506

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 2505	. 2 |- (A = B -> U.A = U.B)
3	1, 2	ax-mp 7	1 |- U.A = U.B

Syntax hints:   = wceq 954  U.cuni 2498

This theorem is referenced by:  elunirab 2509  unisn 2512  unidif0 2734  uniop 2803  reuuni1 2877  reucl 2880  reuuni3 2881  reuunixfr 2901  univ 2904  unisuc 3041  op1sta 3440  op2nda 3444  fv2 3711  funfv2f 3763  funiunfv 3857  elunirn 3859  tfrlem9 3910  tz7.44-2 3920  tz7.44-3 3921  dfrdg2 3924  1st0 4073  2nd0 4074  unielxp 4097  ecqs 4287  xpassen 4427  supex 4557  unir1 4647  rankxplim2 4693  rankxplim3 4694  rankxpsuc 4695  hta 4708  aceq5lem2 4716  kmlem11 4755  infmsup 6023  cbvsum 6932  isumclimtf 7139  isumclt 7152  bastgt 7572  subbas2 7595  fctop 7600  cctop 7602  spwval2 8595  cnlnadjlem5 9942  cnlnadj 9947  adjbdlnt 9954  nmopadjle 9959  cdj3lem3 10299  cdj3lem3b 10301  stoi 10519

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-uni 2499

Copyright terms: Public domain