Theorem limeq 4743

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 4738	. . 3 |- ( A = B -> ( Ord A <-> Ord B ) )
2		neeq1 2628	. . 3 |- ( A = B -> ( A =/= (/) <-> B =/= (/) ) )
3		id 22	. . . 4 |- ( A = B -> A = B )
4		unieq 4111	. . . 4 |- ( A = B -> U. A = U. B )
5	3, 4	eqeq12d 2457	. . 3 |- ( A = B -> ( A = U. A <-> B = U. B ) )
6	1, 2, 5	3anbi123d 1289	. 2 |- ( A = B -> ( ( Ord A /\ A =/= (/) /\ A = U. A ) <-> ( Ord B /\ B =/= (/) /\ B = U. B ) ) )
7		df-lim 4736	. 2 |- ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
8		df-lim 4736	. 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 965   = wceq 1369   =/= wne 2618   (/)c0 3649   U.cuni 4103   Ord word 4730   Lim wlim 4732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-in 3347  df-ss 3354  df-uni 4104  df-tr 4398  df-po 4653  df-so 4654  df-fr 4691  df-we 4693  df-ord 4734  df-lim 4736

This theorem is referenced by:  limuni2  4792  0ellim  4793  limuni3  6475  tfinds2  6486  dfom2  6490  limomss  6493  nnlim  6501  limom  6503  ssnlim  6506  onfununi  6814  tfr1a  6865  tz7.44lem1  6873  tz7.44-2  6875  tz7.44-3  6876  oeeulem  7052  limensuc  7500  elom3  7866  r1funlim  7985  rankxplim2  8099  rankxplim3  8100  rankxpsuc  8101  infxpenlem  8192  alephislim  8265  cflim2  8444  winalim  8874  rankcf  8956  gruina  8997  rdgprc0  27619  dfrdg2  27621  dfrdg4  27993  limsucncmpi  28303  limsucncmp  28304