Theorem limeq 6377

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 6372	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 3004	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4920	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2749	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1437	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6370	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6370	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1088   = wceq 1542   ≠ wne 2941  ∅c0 4323  ∪ cuni 4909  Ord word 6364  Lim wlim 6366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-tr 5267  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-lim 6370

This theorem is referenced by:  limuni2  6427  0ellim  6428  limuni3  7841  tfinds2  7853  dfom2  7857  limomss  7860  nnlim  7869  limom  7871  ssnlim  7875  onfununi  8341  tfr1a  8394  tz7.44lem1  8405  tz7.44-2  8407  tz7.44-3  8408  1ellim  8498  2ellim  8499  oeeulem  8601  limensuc  9154  elom3  9643  r1funlim  9761  rankxplim2  9875  rankxplim3  9876  rankxpsuc  9877  infxpenlem  10008  alephislim  10078  cflim2  10258  winalim  10690  rankcf  10772  gruina  10813  scutbdaybnd2lim  27318  rdgprc0  34765  dfrdg2  34767  dfrdg4  34923  limsucncmpi  35330  limsucncmp  35331  omlimcl2  41991  onexlimgt  41992  onov0suclim  42024  succlg  42078  dflim5  42079  nlim1NEW  42193  nlim2NEW  42194  nlim3  42195  nlim4  42196  dfsucon  42274