Theorem limeq

Description: Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	limeq	$$⊢A=B\to \left(\mathrm{Lim}A\leftrightarrow \mathrm{Lim}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ordeq	$$⊢A=B\to \left(\mathrm{Ord}A\leftrightarrow \mathrm{Ord}B\right)$$
2		neeq1	$$⊢A=B\to \left(A\ne \varnothing \leftrightarrow B\ne \varnothing \right)$$
3		id	$$⊢A=B\to A=B$$
4		unieq	$$⊢A=B\to \bigcup A=\bigcup B$$
5	3 4	eqeq12d	$$⊢A=B\to \left(A=\bigcup A\leftrightarrow B=\bigcup B\right)$$
6	1 2 5	3anbi123d	$$⊢A=B\to \left(\left(\mathrm{Ord}A\wedge A\ne \varnothing \wedge A=\bigcup A\right)\leftrightarrow \left(\mathrm{Ord}B\wedge B\ne \varnothing \wedge B=\bigcup B\right)\right)$$
7		df-lim	$$⊢\mathrm{Lim}A\leftrightarrow \left(\mathrm{Ord}A\wedge A\ne \varnothing \wedge A=\bigcup A\right)$$
8		df-lim	$$⊢\mathrm{Lim}B\leftrightarrow \left(\mathrm{Ord}B\wedge B\ne \varnothing \wedge B=\bigcup B\right)$$
9	6 7 8	3bitr4g	$$⊢A=B\to \left(\mathrm{Lim}A\leftrightarrow \mathrm{Lim}B\right)$$