Theorem unissb 4266

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 4238	. . . . . 6 |- ( y e. U. A <-> E. x ( y e. x /\ x e. A ) )
2	1	imbi1i 323	. . . . 5 |- ( ( y e. U. A -> y e. B ) <-> ( E. x ( y e. x /\ x e. A ) -> y e. B ) )
3		19.23v 1765	. . . . 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 1645	. . 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 1850	. . . 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 1734	. . . . . 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 444	. . . . . . . 8 |- ( ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( y e. x -> ( x e. A -> y e. B ) ) )
9		bi2.04 359	. . . . . . . 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 1645	. . . . . 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 3478	. . . . . . 7 |- ( x C_ B <-> A. y ( y e. x -> y e. B ) )
13	12	imbi2i 310	. . . . . 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 1645	. . . 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 3478	. 2 |- ( U. A C_ B <-> A. y ( y e. U. A -> y e. B ) )
19		df-ral 2809	. 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 367   A.wal 1396   E.wex 1617   e. wcel 1823   A.wral 2804   C_ wss 3461   U.cuni 4235

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-v 3108  df-in 3468  df-ss 3475  df-uni 4236

This theorem is referenced by:  uniss2  4267  ssunieq  4269  sspwuni  4404  pwssb  4405  ordunisssuc  4969  sorpssuni  6562  bm2.5ii  6614  sbthlem1  7620  ordunifi  7762  isfinite2  7770  cflim2  8634  fin23lem16  8706  fin23lem29  8712  fin1a2lem11  8781  fin1a2lem13  8783  itunitc  8792  zorng  8875  wuncval2  9114  suplem1pr  9419  suplem2pr  9420  mrcuni  15110  ipodrsfi  15992  mrelatlub  16015  subgint  16424  efgval  16934  toponmre  19761  neips  19781  neiuni  19790  alexsubALTlem2  20714  alexsubALTlem3  20715  tgpconcompeqg  20776  tglnunirn  24136  uniinn0  27630  locfinreflem  28078  unidmvol  28437  sxbrsigalem0  28479  dya2iocuni  28491  dya2iocucvr  28492  carsguni  28516  ovoliunnfl  30296  voliunnfl  30298  volsupnfl  30299  topjoin  30423  fnejoin1  30426  fnejoin2  30427  intidl  30666  unichnidl  30668