Theorem ex-uni 25445

Description: Example for df-uni 4191. Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016.)

Assertion

Ref	Expression
ex-uni	|- U. { { 1 , 3 } , { 1 , 8 } } = { 1 , 3 , 8 }

Proof of Theorem ex-uni

Step	Hyp	Ref	Expression
1		prex 4632	. . 3 |- { 1 , 3 } e. _V
2		prex 4632	. . 3 |- { 1 , 8 } e. _V
3	1, 2	unipr 4203	. 2 |- U. { { 1 , 3 } , { 1 , 8 } } = ( { 1 , 3 } u. { 1 , 8 } )
4		ex-un 25443	. 2 |- ( { 1 , 3 } u. { 1 , 8 } ) = { 1 , 3 , 8 }
5	3, 4	eqtri 2431	1 |- U. { { 1 , 3 } , { 1 , 8 } } = { 1 , 3 , 8 }

Syntax hints:   = wceq 1405   u. cun 3411   {cpr 3973   {ctp 3975   U.cuni 4190   1c1 9443   3c3 10547   8c8 10552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-sn 3972  df-pr 3974  df-tp 3976  df-uni 4191

This theorem is referenced by: (None)