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\in A\to \forall xy\in A$$
	bnj1316.2	$$⊢y\in B\to \forall xy\in B$$
Assertion	bnj1316	$$⊢A=B\to \bigcup _{x\in A}C=\bigcup _{x\in B}C$$

Proof

Step	Hyp	Ref	Expression
1		bnj1316.1	$$⊢y\in A\to \forall xy\in A$$
2		bnj1316.2	$$⊢y\in B\to \forall xy\in B$$
3	1	nfcii	$$⊢\underset{\_}{Ⅎ}xA$$
4	2	nfcii	$$⊢\underset{\_}{Ⅎ}xB$$
5	3 4	nfeq	$$⊢ℲxA=B$$
6	5	nf5ri	$$⊢A=B\to \forall xA=B$$
7	6	bnj956	$$⊢A=B\to \bigcup _{x\in A}C=\bigcup _{x\in B}C$$