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 3017	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 23	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4877	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2776	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1464	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6370	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6370	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103   = wceq 1569   ≠ wne 2955  ∅c0 4277  ∪ cuni 4866  Ord word 6364  Lim wlim 6366

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-v 3452  df-ss 3897  df-uni 4867  df-tr 5212  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6368  df-lim 6370

This theorem is used by:  limuni2  6429  limuni3  7867  tfinds2  7879  dfom2  7883  limomss  7886  nnlim  7895  limom  7897  ssnlim  7901  onfununi  8357  tfr1a  8410  tz7.44lem1  8421  tz7.44-2  8423  tz7.44-3  8424  1ellim  8514  2ellim  8515  oeeulem  8618  limensuc  9181  elom3  9656  r1funlimOLD  9777  r1dmlim  9779  rankxplim2  9904  rankxplim3  9905  rankxpsuc  9906  infxpenlem  10099  alephislim  10169  cflim2  10348  winalim  10787  rankcf  10869  gruina  10910  cutbdaybnd2lim  28192  rdgprc0  36679  dfrdg2  36681  dfrdg4  36839  limsucncmpi  37357  limsucncmp  37358  omlimcl2  44381  onexlimgt  44382  onov0suclim  44413  succlg  44467  dflim5  44468  nlim1NEW  44580  nlim2NEW  44581  nlim3  44582  nlim4  44583  dfsucon  44661