Theorem bnj1316

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

	Ref	Expression
Hypotheses	bnj1316.1	|- ( y e. A -> A. x y e. A )
	bnj1316.2	|- ( y e. B -> A. x y e. B )
Assertion	bnj1316	|- ( A = B -> U_ x e. A C = U_ x e. B C )

Proof

Step	Hyp	Ref	Expression
1		bnj1316.1	|- ( y e. A -> A. x y e. A )
2		bnj1316.2	|- ( y e. B -> A. x y e. B )
3	1	nfcii	|- F/_ x A
4	2	nfcii	|- F/_ x B
5	3 4	nfeq	|- F/ x A = B
6	5	nf5ri	|- ( A = B -> A. x A = B )
7	6	bnj956	|- ( A = B -> U_ x e. A C = U_ x e. B C )