Theorem unieq 3925

Description: Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Assertion

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

Proof of Theorem unieq

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rexeq 2744	. . 3 |- ( A = B -> ( E. x e. A y e. x <-> E. x e. B y e. x ) )
2	1	abbidv 2354	. 2 |- ( A = B -> { y | E. x e. A y e. x } = { y | E. x e. B y e. x } )
3		dfuni2 3918	. 2 |- U. A = { y | E. x e. A y e. x }
4		dfuni2 3918	. 2 |- U. B = { y | E. x e. B y e. x }
5	2, 3, 4	3eqtr4g 2292	1 |- ( A = B -> U. A = U. B )

Syntax hints:   -> wi 4   = wceq 1398   {cab 2220   E.wrex 2523   U.cuni 3916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-uni 3917

This theorem is referenced by:  unieqi  3926  unieqd  3927  uniintsnr  3987  iununir  4077  treq  4216  limeq  4500  uniex  4560  uniexg  4562  ordsucunielexmid  4655  onsucuni2  4688  nnpredcl  4747  elvvuni  4816  unielrel  5292  unixp0im  5301  iotass  5332  nnsucuniel  6730  en1bg  7042  omp1eom  7388  ctmlemr  7401  nnnninfeq2  7422  uniopn  14883  istopon  14895  eltg3  14939  tgdom  14954  cldval  14981  ntrfval  14982  clsfval  14983  neifval  15022  tgrest  15051  cnprcl2k  15088  bj-uniex  16704  bj-uniexg  16705  nnsf  16800  peano3nninf  16802  exmidsbthr  16820