Metamath Proof Explorer

Theorem bnj956

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

Ref Expression
Hypothesis bnj956.1 ⊢ A = B → ∀ x A = B
Assertion bnj956 ⊢ A = B → ⋃ x ∈ A C = ⋃ x ∈ B C

Proof

Step Hyp Ref Expression
1 bnj956.1 ⊢ A = B → ∀ x A = B
2 eleq2 ⊢ A = B → x ∈ A ↔ x ∈ B
3 2 anbi1d ⊢ A = B → x ∈ A ∧ y ∈ C ↔ x ∈ B ∧ y ∈ C
4 3 alexbii ⊢ ∀ x A = B → ∃ x x ∈ A ∧ y ∈ C ↔ ∃ x x ∈ B ∧ y ∈ C
5 df-rex ⊢ ∃ x ∈ A y ∈ C ↔ ∃ x x ∈ A ∧ y ∈ C
6 df-rex ⊢ ∃ x ∈ B y ∈ C ↔ ∃ x x ∈ B ∧ y ∈ C
7 4 5 6 3bitr4g ⊢ ∀ x A = B → ∃ x ∈ A y ∈ C ↔ ∃ x ∈ B y ∈ C
8 1 7 syl ⊢ A = B → ∃ x ∈ A y ∈ C ↔ ∃ x ∈ B y ∈ C
9 8 abbidv ⊢ A = B → y | ∃ x ∈ A y ∈ C = y | ∃ x ∈ B y ∈ C
10 df-iun ⊢ ⋃ x ∈ A C = y | ∃ x ∈ A y ∈ C
11 df-iun ⊢ ⋃ x ∈ B C = y | ∃ x ∈ B y ∈ C
12 9 10 11 3eqtr4g ⊢ A = B → ⋃ x ∈ A C = ⋃ x ∈ B C