Theorem limeq 4890

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

Assertion

Ref	Expression
limeq	|- ( A = B -> ( Lim A <-> Lim B ) )

Proof of Theorem limeq

Step	Hyp	Ref	Expression
1		ordeq 4885	. . 3 |- ( A = B -> ( Ord A <-> Ord B ) )
2		neeq1 2748	. . 3 |- ( A = B -> ( A =/= (/) <-> B =/= (/) ) )
3		id 22	. . . 4 |- ( A = B -> A = B )
4		unieq 4253	. . . 4 |- ( A = B -> U. A = U. B )
5	3, 4	eqeq12d 2489	. . 3 |- ( A = B -> ( A = U. A <-> B = U. B ) )
6	1, 2, 5	3anbi123d 1299	. 2 |- ( A = B -> ( ( Ord A /\ A =/= (/) /\ A = U. A ) <-> ( Ord B /\ B =/= (/) /\ B = U. B ) ) )
7		df-lim 4883	. 2 |- ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
8		df-lim 4883	. 2 |- ( Lim B <-> ( Ord B /\ B =/= (/) /\ B = U. B ) )
9	6, 7, 8	3bitr4g 288	1 |- ( A = B -> ( Lim A <-> Lim B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ w3a 973   = wceq 1379   =/= wne 2662   (/)c0 3785   U.cuni 4245   Ord word 4877   Lim wlim 4879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-in 3483  df-ss 3490  df-uni 4246  df-tr 4541  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-lim 4883

This theorem is referenced by:  limuni2  4939  0ellim  4940  limuni3  6672  tfinds2  6683  dfom2  6687  limomss  6690  nnlim  6698  limom  6700  ssnlim  6703  onfununi  7013  tfr1a  7064  tz7.44lem1  7072  tz7.44-2  7074  tz7.44-3  7075  oeeulem  7251  limensuc  7695  elom3  8066  r1funlim  8185  rankxplim2  8299  rankxplim3  8300  rankxpsuc  8301  infxpenlem  8392  alephislim  8465  cflim2  8644  winalim  9074  rankcf  9156  gruina  9197  rdgprc0  29079  dfrdg2  29081  dfrdg4  29453  limsucncmpi  29763  limsucncmp  29764