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

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

Proof

Step Hyp Ref Expression
1 bnj956.1 ⊢ ( 𝐴 = 𝐵 → ∀ 𝑥 𝐴 = 𝐵 )
2 eleq2 ⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
3 2 anbi1d ⊢ ( 𝐴 = 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
4 3 alexbii ⊢ ( ∀ 𝑥 𝐴 = 𝐵 → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
5 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) )
6 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
7 4 5 6 3bitr4g ⊢ ( ∀ 𝑥 𝐴 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ) )
8 1 7 syl ⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ) )
9 8 abbidv ⊢ ( 𝐴 = 𝐵 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 } )
10 df-iun ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 }
11 df-iun ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 }
12 9 10 11 3eqtr4g ⊢ ( 𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 )