# 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}\to \forall {x}\phantom{\rule{.4em}{0ex}}{A}={B}$
Assertion bnj956 ${⊢}{A}={B}\to \bigcup _{{x}\in {A}}{C}=\bigcup _{{x}\in {B}}{C}$

### Proof

Step Hyp Ref Expression
1 bnj956.1 ${⊢}{A}={B}\to \forall {x}\phantom{\rule{.4em}{0ex}}{A}={B}$
2 eleq2 ${⊢}{A}={B}\to \left({x}\in {A}↔{x}\in {B}\right)$
3 2 anbi1d ${⊢}{A}={B}\to \left(\left({x}\in {A}\wedge {y}\in {C}\right)↔\left({x}\in {B}\wedge {y}\in {C}\right)\right)$
4 3 alexbii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{A}={B}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {C}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge {y}\in {C}\right)\right)$
5 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {C}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {C}\right)$
6 df-rex ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{y}\in {C}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge {y}\in {C}\right)$
7 4 5 6 3bitr4g ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{A}={B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {C}↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{y}\in {C}\right)$
8 1 7 syl ${⊢}{A}={B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {C}↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{y}\in {C}\right)$
9 8 abbidv ${⊢}{A}={B}\to \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {C}\right\}=\left\{{y}|\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{y}\in {C}\right\}$
10 df-iun ${⊢}\bigcup _{{x}\in {A}}{C}=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {C}\right\}$
11 df-iun ${⊢}\bigcup _{{x}\in {B}}{C}=\left\{{y}|\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{y}\in {C}\right\}$
12 9 10 11 3eqtr4g ${⊢}{A}={B}\to \bigcup _{{x}\in {A}}{C}=\bigcup _{{x}\in {B}}{C}$