Theorem unissb 4469

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 4439	. . . . . 6 |- ( y e. U. A <-> E. x ( y e. x /\ x e. A ) )
2	1	imbi1i 339	. . . . 5 |- ( ( y e. U. A -> y e. B ) <-> ( E. x ( y e. x /\ x e. A ) -> y e. B ) )
3		19.23v 1902	. . . . 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 267	. . . 4 |- ( ( y e. U. A -> y e. B ) <-> A. x ( ( y e. x /\ x e. A ) -> y e. B ) )
5	4	albii 1747	. . 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 2037	. . . 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 1868	. . . . . 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 462	. . . . . . . 8 |- ( ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( y e. x -> ( x e. A -> y e. B ) ) )
9		bi2.04 376	. . . . . . . 8 |- ( ( y e. x -> ( x e. A -> y e. B ) ) <-> ( x e. A -> ( y e. x -> y e. B ) ) )
10	8, 9	bitri 264	. . . . . . 7 |- ( ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( x e. A -> ( y e. x -> y e. B ) ) )
11	10	albii 1747	. . . . . 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 3591	. . . . . . 7 |- ( x C_ B <-> A. y ( y e. x -> y e. B ) )
13	12	imbi2i 326	. . . . . 6 |- ( ( x e. A -> x C_ B ) <-> ( x e. A -> A. y ( y e. x -> y e. B ) ) )
14	7, 11, 13	3bitr4i 292	. . . . 5 |- ( A. y ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( x e. A -> x C_ B ) )
15	14	albii 1747	. . . 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 264	. . 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 264	. 2 |- ( A. y ( y e. U. A -> y e. B ) <-> A. x ( x e. A -> x C_ B ) )
18		dfss2 3591	. 2 |- ( U. A C_ B <-> A. y ( y e. U. A -> y e. B ) )
19		df-ral 2917	. 2 |- ( A. x e. A x C_ B <-> A. x ( x e. A -> x C_ B ) )
20	17, 18, 19	3bitr4i 292	1 |- ( U. A C_ B <-> A. x e. A x C_ B )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704   e. wcel 1990   A.wral 2912   C_ wss 3574   U.cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-in 3581  df-ss 3588  df-uni 4437

This theorem is referenced by:  uniss2  4470  ssunieq  4472  sspwuni  4611  pwssb  4612  ordunisssuc  5830  sorpssuni  6946  bm2.5ii  7006  sbthlem1  8070  ordunifi  8210  isfinite2  8218  cflim2  9085  fin23lem16  9157  fin23lem29  9163  fin1a2lem11  9232  fin1a2lem13  9234  itunitc  9243  zorng  9326  wuncval2  9569  suplem1pr  9874  suplem2pr  9875  mrcuni  16281  ipodrsfi  17163  mrelatlub  17186  subgint  17618  efgval  18130  toponmre  20897  neips  20917  neiuni  20926  alexsubALTlem2  21852  alexsubALTlem3  21853  tgpconncompeqg  21915  unidmvol  23309  tglnunirn  25443  uniinn0  29366  locfinreflem  29907  sxbrsigalem0  30333  dya2iocuni  30345  dya2iocucvr  30346  carsguni  30370  topjoin  32360  fnejoin1  32363  fnejoin2  32364  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  intidl  33828  unichnidl  33830  salexct  40552  setrec1lem2  42435  setrec2fun  42439