cbviung

Description: Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. Usage of this theorem is discouraged because it depends on ax-13 . See cbviun for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by NM, 26-Mar-2006) (Revised by Andrew Salmon, 25-Jul-2011) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbviung.1	$⊢ \underline{Ⅎ} y B$
2		cbviung.2	$⊢ \underline{Ⅎ} x C$
3		cbviung.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	cbvrex	$⊢ \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 cbviung

Proof