Theorem unissb 4198

Description: Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.)

Assertion

Ref	Expression
unissb	|- ( U. A C_ B <-> A. x e. A x C_ B )

Distinct variable groups:   x, A   x, B

Proof of Theorem unissb

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eluni 4170	. . . . . 6 |- ( y e. U. A <-> E. x ( y e. x /\ x e. A ) )
2	1	imbi1i 331	. . . . 5 |- ( ( y e. U. A -> y e. B ) <-> ( E. x ( y e. x /\ x e. A ) -> y e. B ) )
3		19.23v 1821	. . . . 5 |- ( A. x ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( E. x ( y e. x /\ x e. A ) -> y e. B ) )
4	2, 3	bitr4i 260	. . . 4 |- ( ( y e. U. A -> y e. B ) <-> A. x ( ( y e. x /\ x e. A ) -> y e. B ) )
5	4	albii 1694	. . 3 |- ( A. y ( y e. U. A -> y e. B ) <-> A. y A. x ( ( y e. x /\ x e. A ) -> y e. B ) )
6		alcom 1926	. . . 4 |- ( A. y A. x ( ( y e. x /\ x e. A ) -> y e. B ) <-> A. x A. y ( ( y e. x /\ x e. A ) -> y e. B ) )
7		19.21v 1789	. . . . . 6 |- ( A. y ( x e. A -> ( y e. x -> y e. B ) ) <-> ( x e. A -> A. y ( y e. x -> y e. B ) ) )
8		impexp 452	. . . . . . . 8 |- ( ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( y e. x -> ( x e. A -> y e. B ) ) )
9		bi2.04 367	. . . . . . . 8 |- ( ( y e. x -> ( x e. A -> y e. B ) ) <-> ( x e. A -> ( y e. x -> y e. B ) ) )
10	8, 9	bitri 257	. . . . . . 7 |- ( ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( x e. A -> ( y e. x -> y e. B ) ) )
11	10	albii 1694	. . . . . 6 |- ( A. y ( ( y e. x /\ x e. A ) -> y e. B ) <-> A. y ( x e. A -> ( y e. x -> y e. B ) ) )
12		dfss2 3388	. . . . . . 7 |- ( x C_ B <-> A. y ( y e. x -> y e. B ) )
13	12	imbi2i 318	. . . . . 6 |- ( ( x e. A -> x C_ B ) <-> ( x e. A -> A. y ( y e. x -> y e. B ) ) )
14	7, 11, 13	3bitr4i 285	. . . . 5 |- ( A. y ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( x e. A -> x C_ B ) )
15	14	albii 1694	. . . 4 |- ( A. x A. y ( ( y e. x /\ x e. A ) -> y e. B ) <-> A. x ( x e. A -> x C_ B ) )
16	6, 15	bitri 257	. . 3 |- ( A. y A. x ( ( y e. x /\ x e. A ) -> y e. B ) <-> A. x ( x e. A -> x C_ B ) )
17	5, 16	bitri 257	. 2 |- ( A. y ( y e. U. A -> y e. B ) <-> A. x ( x e. A -> x C_ B ) )
18		dfss2 3388	. 2 |- ( U. A C_ B <-> A. y ( y e. U. A -> y e. B ) )
19		df-ral 2741	. 2 |- ( A. x e. A x C_ B <-> A. x ( x e. A -> x C_ B ) )
20	17, 18, 19	3bitr4i 285	1 |- ( U. A C_ B <-> A. x e. A x C_ B )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   A.wal 1445   E.wex 1666   e. wcel 1890   A.wral 2736   C_ wss 3371   U.cuni 4167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2741  df-v 3014  df-in 3378  df-ss 3385  df-uni 4168

This theorem is referenced by:  uniss2  4199  ssunieq  4201  sspwuni  4338  pwssb  4339  ordunisssuc  5503  sorpssuni  6567  bm2.5ii  6620  sbthlem1  7668  ordunifi  7807  isfinite2  7815  cflim2  8679  fin23lem16  8751  fin23lem29  8757  fin1a2lem11  8826  fin1a2lem13  8828  itunitc  8837  zorng  8920  wuncval2  9158  suplem1pr  9463  suplem2pr  9464  mrcuni  15537  ipodrsfi  16419  mrelatlub  16442  subgint  16851  efgval  17377  toponmre  20119  neips  20139  neiuni  20148  alexsubALTlem2  21073  alexsubALTlem3  21074  tgpconcompeqg  21136  unidmvol  22505  tglnunirn  24604  uniinn0  28173  locfinreflem  28673  sxbrsigalem0  29098  dya2iocuni  29110  dya2iocucvr  29111  carsguni  29145  topjoin  31026  fnejoin1  31029  fnejoin2  31030  ovoliunnfl  31983  voliunnfl  31985  volsupnfl  31986  intidl  32263  unichnidl  32265  salexct  38249