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	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
	bnj1316.2	⊢ ( 𝑦 ∈ 𝐵 → ∀ 𝑥 𝑦 ∈ 𝐵 )
Assertion	bnj1316	⊢ ( 𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		bnj1316.1	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
2		bnj1316.2	⊢ ( 𝑦 ∈ 𝐵 → ∀ 𝑥 𝑦 ∈ 𝐵 )
3	1	nfcii	⊢ Ⅎ 𝑥 𝐴
4	2	nfcii	⊢ Ⅎ 𝑥 𝐵
5	3 4	nfeq	⊢ Ⅎ 𝑥 𝐴 = 𝐵
6	5	nf5ri	⊢ ( 𝐴 = 𝐵 → ∀ 𝑥 𝐴 = 𝐵 )
7	6	bnj956	⊢ ( 𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 )