This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ A → ∀ x y ∈ A
bnj1316.2 ⊢ y ∈ B → ∀ x y ∈ B
Assertion bnj1316 ⊢ A = B → ⋃ x ∈ A C = ⋃ x ∈ B C

Proof

Step Hyp Ref Expression
1 bnj1316.1 ⊢ y ∈ A → ∀ x y ∈ A
2 bnj1316.2 ⊢ y ∈ B → ∀ x y ∈ B
3 1 nfcii ⊢ Ⅎ _ x A
4 2 nfcii ⊢ Ⅎ _ x B
5 3 4 nfeq ⊢ Ⅎ x A = B
6 5 nf5ri ⊢ A = B → ∀ x A = B
7 6 bnj956 ⊢ A = B → ⋃ x ∈ A C = ⋃ x ∈ B C