supeq1

Description: Equality theorem for supremum. (Contributed by NM, 22-May-1999)

		Ref	Expression
	Assertion	supeq1	$⊢ B = C \to sup (B, A, R) = sup (C, A, R)$

Step	Hyp	Ref	Expression
1		raleq	$⊢ B = C \to (\forall y \in B \neg x R y \leftrightarrow \forall y \in C \neg x R y)$
2		rexeq	$⊢ B = C \to (\exists z \in B y R z \leftrightarrow \exists z \in C y R z)$
3	2	imbi2d	$⊢ B = C \to ((y R x \to \exists z \in B y R z) \leftrightarrow (y R x \to \exists z \in C y R z))$
4	3	ralbidv	$⊢ B = C \to (\forall y \in A (y R x \to \exists z \in B y R z) \leftrightarrow \forall y \in A (y R x \to \exists z \in C y R z))$
5	1 4	anbi12d	$⊢ B = C \to ((\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \leftrightarrow (\forall y \in C \neg x R y \land \forall y \in A (y R x \to \exists z \in C y R z)))$
6	5	rabbidv	$⊢ B = C \to \{x \in A \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\} = \{x \in A \| (\forall y \in C \neg x R y \land \forall y \in A (y R x \to \exists z \in C y R z))\}$
7	6	unieqd	$⊢ B = C \to ⋃ \{x \in A \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\} = ⋃ \{x \in A \| (\forall y \in C \neg x R y \land \forall y \in A (y R x \to \exists z \in C y R z))\}$
8		df-sup	$⊢ sup (B, A, R) = ⋃ \{x \in A \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\}$
9		df-sup	$⊢ sup (C, A, R) = ⋃ \{x \in A \| (\forall y \in C \neg x R y \land \forall y \in A (y R x \to \exists z \in C y R z))\}$
10	7 8 9	3eqtr4g	$⊢ B = C \to sup (B, A, R) = sup (C, A, R)$

Metamath Proof Explorer