Theorem limeq 6374

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 6369	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 3018	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 23	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4878	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2777	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1464	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6367	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6367	. 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 1570   ≠ wne 2956  ∅c0 4279  ∪ cuni 4867  Ord word 6361  Lim wlim 6363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-v 3453  df-ss 3916  df-uni 4868  df-tr 5213  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6365  df-lim 6367

This theorem is used by:  limuni2  6426  limuni3  7863  tfinds2  7875  dfom2  7879  limomss  7882  nnlim  7891  limom  7893  ssnlim  7897  onfununi  8349  tfr1a  8402  tz7.44lem1  8413  tz7.44-2  8415  tz7.44-3  8416  1ellim  8506  2ellim  8507  oeeulem  8610  limensuc  9173  elom3  9649  r1funlimOLD  9770  r1dmlim  9772  rankxplim2  9897  rankxplim3  9898  rankxpsuc  9899  infxpenlem  10092  alephislim  10162  cflim2  10341  winalim  10780  rankcf  10862  gruina  10903  cutbdaybnd2lim  28183  rdgprc0  36555  dfrdg2  36557  dfrdg4  36715  limsucncmpi  37233  limsucncmp  37234  omlimcl2  44243  onexlimgt  44244  onov0suclim  44275  succlg  44329  dflim5  44330  nlim1NEW  44442  nlim2NEW  44443  nlim3  44444  nlim4  44445  dfsucon  44523