cbviun

Description: Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006) (Revised by Andrew Salmon, 25-Jul-2011) Add disjoint variable condition to avoid ax-13 . See cbviung for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024)

	Ref	Expression
Hypotheses	cbviun.1	$⊢ \underline{Ⅎ} y B$
	cbviun.2	$⊢ \underline{Ⅎ} x C$
	cbviun.3	$⊢ x = y \to B = C$
Assertion	cbviun	$⊢ ⋃_{x \in A} B = ⋃_{y \in A} C$

Proof

Step	Hyp	Ref	Expression
1		cbviun.1	$⊢ \underline{Ⅎ} y B$
2		cbviun.2	$⊢ \underline{Ⅎ} x C$
3		cbviun.3	$⊢ x = y \to B = C$
4	1	nfcri	$⊢ Ⅎ y z \in B$
5	2	nfcri	$⊢ Ⅎ x z \in C$
6	3	eleq2d	$⊢ x = y \to (z \in B \leftrightarrow z \in C)$
7	4 5 6	cbvrexw	$⊢ \exists x \in A z \in B \leftrightarrow \exists y \in A z \in C$
8	7	abbii	$⊢ \{z \| \exists x \in A z \in B\} = \{z \| \exists y \in A z \in C\}$
9		df-iun	$⊢ ⋃_{x \in A} B = \{z \| \exists x \in A z \in B\}$
10		df-iun	$⊢ ⋃_{y \in A} C = \{z \| \exists y \in A z \in C\}$
11	8 9 10	3eqtr4i	$⊢ ⋃_{x \in A} B = ⋃_{y \in A} C$

Metamath Proof Explorer

Theorem cbviun

Proof