Theorem iotaeq

Description: Equality theorem for descriptions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 30-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	iotaeq	$$⊢\forall xx=y\to \left(\iota x|\phi \right)=\left(\iota y|\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		drsb1	$$⊢\forall xx=y\to \left(\left[z/x\right]\phi \leftrightarrow \left[z/y\right]\phi \right)$$
2		df-clab	$$⊢z\in \left\{x|\phi \right\}\leftrightarrow \left[z/x\right]\phi$$
3		df-clab	$$⊢z\in \left\{y|\phi \right\}\leftrightarrow \left[z/y\right]\phi$$
4	1 2 3	3bitr4g	$$⊢\forall xx=y\to \left(z\in \left\{x|\phi \right\}\leftrightarrow z\in \left\{y|\phi \right\}\right)$$
5	4	eqrdv	$$⊢\forall xx=y\to \left\{x|\phi \right\}=\left\{y|\phi \right\}$$
6	5	eqeq1d	$$⊢\forall xx=y\to \left(\left\{x|\phi \right\}=\left\{z\right\}\leftrightarrow \left\{y|\phi \right\}=\left\{z\right\}\right)$$
7	6	abbidv	$$⊢\forall xx=y\to \left\{z|\left\{x|\phi \right\}=\left\{z\right\}\right\}=\left\{z|\left\{y|\phi \right\}=\left\{z\right\}\right\}$$
8	7	unieqd	$$⊢\forall xx=y\to \bigcup \left\{z|\left\{x|\phi \right\}=\left\{z\right\}\right\}=\bigcup \left\{z|\left\{y|\phi \right\}=\left\{z\right\}\right\}$$
9		df-iota	$$⊢\left(\iota x|\phi \right)=\bigcup \left\{z|\left\{x|\phi \right\}=\left\{z\right\}\right\}$$
10		df-iota	$$⊢\left(\iota y|\phi \right)=\bigcup \left\{z|\left\{y|\phi \right\}=\left\{z\right\}\right\}$$
11	8 9 10	3eqtr4g	$$⊢\forall xx=y\to \left(\iota x|\phi \right)=\left(\iota y|\phi \right)$$