Theorem unissb

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

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

Proof

Step	Hyp	Ref	Expression
1		eluni	|- ( y e. U. A <-> E. x ( y e. x /\ x e. A ) )
2	1	imbi1i	|- ( ( y e. U. A -> y e. B ) <-> ( E. x ( y e. x /\ x e. A ) -> y e. B ) )
3		19.23v	|- ( 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	|- ( ( y e. U. A -> y e. B ) <-> A. x ( ( y e. x /\ x e. A ) -> y e. B ) )
5	4	albii	|- ( A. y ( y e. U. A -> y e. B ) <-> A. y A. x ( ( y e. x /\ x e. A ) -> y e. B ) )
6		alcom	|- ( 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	|- ( A. y ( x e. A -> ( y e. x -> y e. B ) ) <-> ( x e. A -> A. y ( y e. x -> y e. B ) ) )
8		impexp	|- ( ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( y e. x -> ( x e. A -> y e. B ) ) )
9		bi2.04	|- ( ( y e. x -> ( x e. A -> y e. B ) ) <-> ( x e. A -> ( y e. x -> y e. B ) ) )
10	8 9	bitri	|- ( ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( x e. A -> ( y e. x -> y e. B ) ) )
11	10	albii	|- ( A. y ( ( y e. x /\ x e. A ) -> y e. B ) <-> A. y ( x e. A -> ( y e. x -> y e. B ) ) )
12		dfss2	|- ( x C_ B <-> A. y ( y e. x -> y e. B ) )
13	12	imbi2i	|- ( ( x e. A -> x C_ B ) <-> ( x e. A -> A. y ( y e. x -> y e. B ) ) )
14	7 11 13	3bitr4i	|- ( A. y ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( x e. A -> x C_ B ) )
15	14	albii	|- ( 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	|- ( 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	|- ( A. y ( y e. U. A -> y e. B ) <-> A. x ( x e. A -> x C_ B ) )
18		dfss2	|- ( U. A C_ B <-> A. y ( y e. U. A -> y e. B ) )
19		df-ral	|- ( A. x e. A x C_ B <-> A. x ( x e. A -> x C_ B ) )
20	17 18 19	3bitr4i	|- ( U. A C_ B <-> A. x e. A x C_ B )