Theorem limeq 6369

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 6364	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 3017	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 23	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4878	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2776	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1464	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6362	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6362	. 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 2955  ∅c0 4279  ∪ cuni 4867  Ord word 6356  Lim wlim 6358

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-v 3452  df-ss 3916  df-uni 4868  df-tr 5213  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6360  df-lim 6362

This theorem is used by:  limuni2  6421  limuni3  7849  tfinds2  7861  dfom2  7865  limomss  7868  nnlim  7877  limom  7879  ssnlim  7883  onfununi  8331  tfr1a  8384  tz7.44lem1  8395  tz7.44-2  8397  tz7.44-3  8398  1ellim  8486  2ellim  8487  oeeulem  8590  limensuc  9153  elom3  9628  r1funlim  9749  rankxplim2  9863  rankxplim3  9864  rankxpsuc  9865  infxpenlem  10017  alephislim  10087  cflim2  10266  winalim  10705  rankcf  10787  gruina  10828  cutbdaybnd2lim  28063  rdgprc0  36371  dfrdg2  36373  dfrdg4  36531  limsucncmpi  37065  limsucncmp  37066  omlimcl2  44084  onexlimgt  44085  onov0suclim  44116  succlg  44170  dflim5  44171  nlim1NEW  44283  nlim2NEW  44284  nlim3  44285  nlim4  44286  dfsucon  44364