Theorem unissb 4232

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 4203	. . . . . 6 |- ( y e. U. A <-> E. x ( y e. x /\ x e. A ) )
2	1	imbi1i 325	. . . . 5 |- ( ( y e. U. A -> y e. B ) <-> ( E. x ( y e. x /\ x e. A ) -> y e. B ) )
3		19.23v 1922	. . . . 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 252	. . . 4 |- ( ( y e. U. A -> y e. B ) <-> A. x ( ( y e. x /\ x e. A ) -> y e. B ) )
5	4	albii 1611	. . 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 1785	. . . 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 1921	. . . . . 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 446	. . . . . . . 8 |- ( ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( y e. x -> ( x e. A -> y e. B ) ) )
9		bi2.04 361	. . . . . . . 8 |- ( ( y e. x -> ( x e. A -> y e. B ) ) <-> ( x e. A -> ( y e. x -> y e. B ) ) )
10	8, 9	bitri 249	. . . . . . 7 |- ( ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( x e. A -> ( y e. x -> y e. B ) ) )
11	10	albii 1611	. . . . . 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 3454	. . . . . . 7 |- ( x C_ B <-> A. y ( y e. x -> y e. B ) )
13	12	imbi2i 312	. . . . . 6 |- ( ( x e. A -> x C_ B ) <-> ( x e. A -> A. y ( y e. x -> y e. B ) ) )
14	7, 11, 13	3bitr4i 277	. . . . 5 |- ( A. y ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( x e. A -> x C_ B ) )
15	14	albii 1611	. . . 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 249	. . 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 249	. 2 |- ( A. y ( y e. U. A -> y e. B ) <-> A. x ( x e. A -> x C_ B ) )
18		dfss2 3454	. 2 |- ( U. A C_ B <-> A. y ( y e. U. A -> y e. B ) )
19		df-ral 2804	. 2 |- ( A. x e. A x C_ B <-> A. x ( x e. A -> x C_ B ) )
20	17, 18, 19	3bitr4i 277	1 |- ( U. A C_ B <-> A. x e. A x C_ B )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1368   E.wex 1587   e. wcel 1758   A.wral 2799   C_ wss 3437   U.cuni 4200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-v 3080  df-in 3444  df-ss 3451  df-uni 4201

This theorem is referenced by:  uniss2  4233  ssunieq  4235  sspwuni  4365  pwssb  4366  ordunisssuc  4930  sorpssuni  6480  bm2.5ii  6528  sbthlem1  7532  ordunifi  7674  isfinite2  7682  cflim2  8544  fin23lem16  8616  fin23lem29  8622  fin1a2lem11  8691  fin1a2lem13  8693  itunitc  8702  zorng  8785  wuncval2  9026  suplem1pr  9333  suplem2pr  9334  mrcuni  14679  ipodrsfi  15453  mrelatlub  15476  subgint  15825  efgval  16336  toponmre  18830  neips  18850  neiuni  18859  alexsubALTlem2  19753  alexsubALTlem3  19754  tgpconcompeqg  19815  tglnunirn  23119  unidmvol  26789  sxbrsigalem0  26831  dya2iocuni  26843  dya2iocucvr  26844  ovoliunnfl  28582  voliunnfl  28584  volsupnfl  28585  topjoin  28735  fnejoin1  28738  fnejoin2  28739  intidl  28978  unichnidl  28980