Theorem bnj1146

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

	Ref	Expression
Hypothesis	bnj1146.1	|- ( y e. A -> A. x y e. A )
Assertion	bnj1146	|- U_ x e. A B C_ B

Proof

Step	Hyp	Ref	Expression
1		bnj1146.1	|- ( y e. A -> A. x y e. A )
2		nfv	|- F/ y ( x e. A /\ w e. B )
3	1	nf5i	|- F/ x y e. A
4		nfv	|- F/ x w e. B
5	3 4	nfan	|- F/ x ( y e. A /\ w e. B )
6		eleq1w	|- ( x = y -> ( x e. A <-> y e. A ) )
7	6	anbi1d	|- ( x = y -> ( ( x e. A /\ w e. B ) <-> ( y e. A /\ w e. B ) ) )
8	2 5 7	cbvexv1	|- ( E. x ( x e. A /\ w e. B ) <-> E. y ( y e. A /\ w e. B ) )
9		df-rex	|- ( E. x e. A w e. B <-> E. x ( x e. A /\ w e. B ) )
10		df-rex	|- ( E. y e. A w e. B <-> E. y ( y e. A /\ w e. B ) )
11	8 9 10	3bitr4i	|- ( E. x e. A w e. B <-> E. y e. A w e. B )
12	11	abbii	|- { w | E. x e. A w e. B } = { w | E. y e. A w e. B }
13		df-iun	|- U_ x e. A B = { w | E. x e. A w e. B }
14		df-iun	|- U_ y e. A B = { w | E. y e. A w e. B }
15	12 13 14	3eqtr4i	|- U_ x e. A B = U_ y e. A B
16		bnj1143	|- U_ y e. A B C_ B
17	15 16	eqsstri	|- U_ x e. A B C_ B