Theorem unieq 3657

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 2563	. . 3 |- ( A = B -> ( E. x e. A y e. x <-> E. x e. B y e. x ) )
2	1	abbidv 2205	. 2 |- ( A = B -> { y | E. x e. A y e. x } = { y | E. x e. B y e. x } )
3		dfuni2 3650	. 2 |- U. A = { y | E. x e. A y e. x }
4		dfuni2 3650	. 2 |- U. B = { y | E. x e. B y e. x }
5	2, 3, 4	3eqtr4g 2145	1 |- ( A = B -> U. A = U. B )

Syntax hints:   -> wi 4   = wceq 1289   {cab 2074   E.wrex 2360   U.cuni 3648

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rex 2365  df-uni 3649

This theorem is referenced by:  unieqi  3658  unieqd  3659  uniintsnr  3719  iununir  3807  treq  3934  limeq  4195  uniex  4255  uniexg  4256  ordsucunielexmid  4337  onsucuni2  4370  elvvuni  4490  unielrel  4945  unixp0im  4954  iotass  4984  nnsucuniel  6238  en1bg  6497  bj-uniex  11454  bj-uniexg  11455  nnpredcl  11536  nnsf  11541  peano3nninf  11543  exmidsbthr  11559