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 A = B$
	Assertion	bnj956	$⊢ A = B \to ⋃_{x \in A} C = ⋃_{x \in B} C$

Step	Hyp	Ref	Expression
1		bnj956.1	$⊢ A = B \to \forall x A = B$
2		eleq2	$⊢ A = B \to (x \in A \leftrightarrow x \in B)$
3	2	anbi1d	$⊢ A = B \to ((x \in A \land y \in C) \leftrightarrow (x \in B \land y \in C))$
4	3	alexbii	$⊢ \forall x A = B \to (\exists x (x \in A \land y \in C) \leftrightarrow \exists x (x \in B \land y \in C))$
5		df-rex	$⊢ \exists x \in A y \in C \leftrightarrow \exists x (x \in A \land y \in C)$
6		df-rex	$⊢ \exists x \in B y \in C \leftrightarrow \exists x (x \in B \land y \in C)$
7	4 5 6	3bitr4g	$⊢ \forall x A = B \to (\exists x \in A y \in C \leftrightarrow \exists x \in B y \in C)$
8	1 7	syl	$⊢ A = B \to (\exists x \in A y \in C \leftrightarrow \exists x \in B y \in C)$
9	8	abbidv	$⊢ A = B \to \{y \| \exists x \in A y \in C\} = \{y \| \exists x \in B y \in C\}$
10		df-iun	$⊢ ⋃_{x \in A} C = \{y \| \exists x \in A y \in C\}$
11		df-iun	$⊢ ⋃_{x \in B} C = \{y \| \exists x \in B y \in C\}$
12	9 10 11	3eqtr4g	$⊢ A = B \to ⋃_{x \in A} C = ⋃_{x \in B} C$

Metamath Proof Explorer