Theorem unissb 4005

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 3978	. . . . . 6 |- ( y e. U. A <-> E. x ( y e. x /\ x e. A ) )
2	1	imbi1i 316	. . . . 5 |- ( ( y e. U. A -> y e. B ) <-> ( E. x ( y e. x /\ x e. A ) -> y e. B ) )
3		19.23v 1910	. . . . 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 244	. . . 4 |- ( ( y e. U. A -> y e. B ) <-> A. x ( ( y e. x /\ x e. A ) -> y e. B ) )
5	4	albii 1572	. . 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 1748	. . . 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 1909	. . . . . 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 434	. . . . . . . 8 |- ( ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( y e. x -> ( x e. A -> y e. B ) ) )
9		bi2.04 351	. . . . . . . 8 |- ( ( y e. x -> ( x e. A -> y e. B ) ) <-> ( x e. A -> ( y e. x -> y e. B ) ) )
10	8, 9	bitri 241	. . . . . . 7 |- ( ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( x e. A -> ( y e. x -> y e. B ) ) )
11	10	albii 1572	. . . . . 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 3297	. . . . . . 7 |- ( x C_ B <-> A. y ( y e. x -> y e. B ) )
13	12	imbi2i 304	. . . . . 6 |- ( ( x e. A -> x C_ B ) <-> ( x e. A -> A. y ( y e. x -> y e. B ) ) )
14	7, 11, 13	3bitr4i 269	. . . . 5 |- ( A. y ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( x e. A -> x C_ B ) )
15	14	albii 1572	. . . 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 241	. . 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 241	. 2 |- ( A. y ( y e. U. A -> y e. B ) <-> A. x ( x e. A -> x C_ B ) )
18		dfss2 3297	. 2 |- ( U. A C_ B <-> A. y ( y e. U. A -> y e. B ) )
19		df-ral 2671	. 2 |- ( A. x e. A x C_ B <-> A. x ( x e. A -> x C_ B ) )
20	17, 18, 19	3bitr4i 269	1 |- ( U. A C_ B <-> A. x e. A x C_ B )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   A.wal 1546   E.wex 1547   e. wcel 1721   A.wral 2666   C_ wss 3280   U.cuni 3975

This theorem is referenced by:  uniss2  4006  ssunieq  4008  sspwuni  4136  pwssb  4137  ordunisssuc  4643  bm2.5ii  4745  sorpssuni  6490  sbthlem1  7176  ordunifi  7316  isfinite2  7324  cflim2  8099  fin23lem16  8171  fin23lem29  8177  fin1a2lem11  8246  fin1a2lem13  8248  itunitc  8257  zorng  8340  wuncval2  8578  suplem1pr  8885  suplem2pr  8886  mrcuni  13801  ipodrsfi  14544  mrelatlub  14567  subgint  14919  efgval  15304  toponmre  17112  neips  17132  neiuni  17141  alexsubALTlem2  18032  alexsubALTlem3  18033  tgpconcompeqg  18094  unidmvol  24537  sxbrsigalem0  24574  dya2iocuni  24586  dya2iocucvr  24587  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  topjoin  26284  fnejoin1  26287  fnejoin2  26288  intidl  26529  unichnidl  26531

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-v 2918  df-in 3287  df-ss 3294  df-uni 3976