Theorem unieq 2510

Description: Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18.

Assertion

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

Proof of Theorem unieq

Step	Hyp	Ref	Expression
1		eleq2 1535	. . . . 5 |- (A = B -> (y e. A <-> y e. B))
2	1	anbi2d 616	. . . 4 |- (A = B -> ((x e. y /\ y e. A) <-> (x e. y /\ y e. B)))
3	2	exbidv 1279	. . 3 |- (A = B -> (E.y(x e. y /\ y e. A) <-> E.y(x e. y /\ y e. B)))
4	3	abbidv 1577	. 2 |- (A = B -> {x | E.y(x e. y /\ y e. A)} = {x | E.y(x e. y /\ y e. B)})
5		df-uni 2504	. 2 |- U.A = {x | E.y(x e. y /\ y e. A)}
6		df-uni 2504	. 2 |- U.B = {x | E.y(x e. y /\ y e. B)}
7	4, 5, 6	3eqtr4g 1531	1 |- (A = B -> U.A = U.B)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 956   e. wcel 958  E.wex 980  {cab 1463  U.cuni 2503

This theorem is referenced by:  unieqi 2511  unieqd 2512  treq 2686  uniex 2870  uniexg 2871  euuni 2881  reucl 2885  rabsnt 2894  reuunisn 2895  limeq 2960  ordunisuc 3089  onsucuni2 3091  onuninsuc 3108  unizlim 3113  orduninsuc 3114  elvvuni 3229  unielrel 3514  unixp0 3518  fvex 3732  tz7.44-2 3929  rdglem2 3938  unifiOLD 4557  infeq5 4621  trcl 4645  rankuni 4698  rankxplim3 4714  unidomg 4809  dominf 4904  uniopnt 7598  eltopsp 7604  tpsex 7605  istps 7606  tgval3t 7625  subtop 7646  sn0top 7647  indistop 7648  cldval 7666  ntrfval 7667  clsfval 7668  neifval 7714  lpfval 7742  cnfval 7756  cnpfval 7757  ishaus 7783  isps 8645  spwval2 8653  hsupval2t 9300  homeofval 10516  qusp 10555  isfil 10558  sfvlim 10605  sfvlimOLD 10606  limfillem2OLD 10608  ist1 10614

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-uni 2504

Copyright terms: Public domain