Theorem bnj1400

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

	Ref	Expression
Hypothesis	bnj1400.1	|- ( y e. A -> A. x y e. A )
Assertion	bnj1400	|- dom U. A = U_ x e. A dom x

Proof

Step	Hyp	Ref	Expression
1		bnj1400.1	|- ( y e. A -> A. x y e. A )
2		dmuni	|- dom U. A = U_ z e. A dom z
3		df-iun	|- U_ x e. A dom x = { y | E. x e. A y e. dom x }
4		df-iun	|- U_ z e. A dom z = { y | E. z e. A y e. dom z }
5	1	nfcii	|- F/_ x A
6		nfcv	|- F/_ z A
7		nfv	|- F/ z y e. dom x
8		nfv	|- F/ x y e. dom z
9		dmeq	|- ( x = z -> dom x = dom z )
10	9	eleq2d	|- ( x = z -> ( y e. dom x <-> y e. dom z ) )
11	5 6 7 8 10	cbvrexfw	|- ( E. x e. A y e. dom x <-> E. z e. A y e. dom z )
12	11	abbii	|- { y | E. x e. A y e. dom x } = { y | E. z e. A y e. dom z }
13	4 12	eqtr4i	|- U_ z e. A dom z = { y | E. x e. A y e. dom x }
14	3 13	eqtr4i	|- U_ x e. A dom x = U_ z e. A dom z
15	2 14	eqtr4i	|- dom U. A = U_ x e. A dom x