Theorem unieq 2514

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 1538	. . . . 5 |- (A = B -> (y e. A <-> y e. B))
2	1	anbi2d 618	. . . 4 |- (A = B -> ((x e. y /\ y e. A) <-> (x e. y /\ y e. B)))
3	2	exbidv 1281	. . 3 |- (A = B -> (E.y(x e. y /\ y e. A) <-> E.y(x e. y /\ y e. B)))
4	3	abbidv 1580	. 2 |- (A = B -> {x | E.y(x e. y /\ y e. A)} = {x | E.y(x e. y /\ y e. B)})
5		df-uni 2508	. 2 |- U.A = {x | E.y(x e. y /\ y e. A)}
6		df-uni 2508	. 2 |- U.B = {x | E.y(x e. y /\ y e. B)}
7	4, 5, 6	3eqtr4g 1534	1 |- (A = B -> U.A = U.B)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 958   e. wcel 960  E.wex 982  {cab 1466  U.cuni 2507

This theorem is referenced by:  unieqi 2515  unieqd 2516  treq 2691  uniex 2876  uniexg 2877  euuni 2887  reucl 2891  rabsnt 2900  reuunisn 2901  limeq 2966  ordunisuc 3095  onsucuni2 3097  onuninsuc 3114  unizlim 3119  orduninsuc 3120  elvvuni 3235  unielrel 3520  unixp0 3524  fvex 3738  tz7.44-2 3935  rdglem2 3944  unifiOLD 4570  infeq5 4630  trcl 4655  rankuni 4708  rankxplim3 4724  unidomg 4819  dominf 4915  dominfOLD 4916  uniopnt 7599  eltopsp 7605  tpsex 7606  istps 7607  tgval3t 7624  subtop 7643  sn0top 7644  indistop 7645  cldval 7663  ntrfval 7664  clsfval 7665  neifval 7711  lpfval 7739  cnfval 7753  cnpfval 7754  ishaus 7780  isps 8641  spwval2 8649  hsupval2t 9295  homeofval 10502  qusp 10541  isfil 10544  sfvlim 10576  sfvlimOLD 10577  limfillem2OLD 10579  ist1 10585

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