Theorem limeq 6373

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	⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Proof of Theorem limeq

Step	Hyp	Ref	Expression
1		ordeq 6368	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 3026	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 23	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4887	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2785	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1462	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6366	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6366	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101   = wceq 1567   ≠ wne 2964  ∅c0 4294  ∪ cuni 4876  Ord word 6360  Lim wlim 6362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-v 3465  df-ss 3930  df-uni 4877  df-tr 5223  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-ord 6364  df-lim 6366

This theorem is referenced by:  limuni2  6425  limuni3  7847  tfinds2  7859  dfom2  7863  limomss  7866  nnlim  7875  limom  7877  ssnlim  7881  onfununi  8327  tfr1a  8380  tz7.44lem1  8391  tz7.44-2  8393  tz7.44-3  8394  1ellim  8482  2ellim  8483  oeeulem  8586  limensuc  9141  elom3  9616  r1funlim  9737  rankxplim2  9851  rankxplim3  9852  rankxpsuc  9853  infxpenlem  9996  alephislim  10066  cflim2  10246  winalim  10679  rankcf  10761  gruina  10802  cutbdaybnd2lim  27955  rdgprc0  36181  dfrdg2  36183  dfrdg4  36341  limsucncmpi  36844  limsucncmp  36845  omlimcl2  43860  onexlimgt  43861  onov0suclim  43892  succlg  43946  dflim5  43947  nlim1NEW  44059  nlim2NEW  44060  nlim3  44061  nlim4  44062  dfsucon  44140