Description: Equality theorem for class union. Exercise 15 of TakeutiZaring p. 18. (Contributed by NM, 10-Aug-1993) (Proof shortened by Andrew Salmon, 29-Jun-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | unieq | ⊢ ( 𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rexeq | ⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ) ) | |
| 2 | 1 | abbidv | ⊢ ( 𝐴 = 𝐵 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 } ) |
| 3 | dfuni2 | ⊢ ∪ 𝐴 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 } | |
| 4 | dfuni2 | ⊢ ∪ 𝐵 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 } | |
| 5 | 2 3 4 | 3eqtr4g | ⊢ ( 𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵 ) |