Theorem bnj1143

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	bnj1143	|- U_ x e. A B C_ B

Proof

Step	Hyp	Ref	Expression
1		df-iun	|- U_ x e. A B = { y | E. x e. A y e. B }
2		notnotb	|- ( A = (/) <-> -. -. A = (/) )
3		neq0	|- ( -. A = (/) <-> E. x x e. A )
4	2 3	xchbinx	|- ( A = (/) <-> -. E. x x e. A )
5		df-rex	|- ( E. x e. A z e. B <-> E. x ( x e. A /\ z e. B ) )
6		exsimpl	|- ( E. x ( x e. A /\ z e. B ) -> E. x x e. A )
7	5 6	sylbi	|- ( E. x e. A z e. B -> E. x x e. A )
8	7	con3i	|- ( -. E. x x e. A -> -. E. x e. A z e. B )
9	4 8	sylbi	|- ( A = (/) -> -. E. x e. A z e. B )
10	9	alrimiv	|- ( A = (/) -> A. z -. E. x e. A z e. B )
11		notnotb	|- ( { y | E. x e. A y e. B } = (/) <-> -. -. { y | E. x e. A y e. B } = (/) )
12		neq0	|- ( -. U_ x e. A B = (/) <-> E. z z e. U_ x e. A B )
13	1	eqeq1i	|- ( U_ x e. A B = (/) <-> { y | E. x e. A y e. B } = (/) )
14	13	notbii	|- ( -. U_ x e. A B = (/) <-> -. { y | E. x e. A y e. B } = (/) )
15		df-iun	|- U_ x e. A B = { z | E. x e. A z e. B }
16	15	eleq2i	|- ( z e. U_ x e. A B <-> z e. { z | E. x e. A z e. B } )
17	16	exbii	|- ( E. z z e. U_ x e. A B <-> E. z z e. { z | E. x e. A z e. B } )
18	12 14 17	3bitr3i	|- ( -. { y | E. x e. A y e. B } = (/) <-> E. z z e. { z | E. x e. A z e. B } )
19	11 18	xchbinx	|- ( { y | E. x e. A y e. B } = (/) <-> -. E. z z e. { z | E. x e. A z e. B } )
20		alnex	|- ( A. z -. z e. { z | E. x e. A z e. B } <-> -. E. z z e. { z | E. x e. A z e. B } )
21		abid	|- ( z e. { z | E. x e. A z e. B } <-> E. x e. A z e. B )
22	21	notbii	|- ( -. z e. { z | E. x e. A z e. B } <-> -. E. x e. A z e. B )
23	22	albii	|- ( A. z -. z e. { z | E. x e. A z e. B } <-> A. z -. E. x e. A z e. B )
24	19 20 23	3bitr2i	|- ( { y | E. x e. A y e. B } = (/) <-> A. z -. E. x e. A z e. B )
25	10 24	sylibr	|- ( A = (/) -> { y | E. x e. A y e. B } = (/) )
26	1 25	syl5eq	|- ( A = (/) -> U_ x e. A B = (/) )
27		0ss	|- (/) C_ B
28	26 27	eqsstrdi	|- ( A = (/) -> U_ x e. A B C_ B )
29		iunconst	|- ( A =/= (/) -> U_ x e. A B = B )
30		eqimss	|- ( U_ x e. A B = B -> U_ x e. A B C_ B )
31	29 30	syl	|- ( A =/= (/) -> U_ x e. A B C_ B )
32	28 31	pm2.61ine	|- U_ x e. A B C_ B