Theorem limeq 6376

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 6371	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 3022	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 23	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4885	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2781	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1464	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6369	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6369	. 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 2960  ∅c0 4286  ∪ cuni 4874  Ord word 6363  Lim wlim 6365

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-v 3459  df-ss 3923  df-uni 4875  df-tr 5221  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-lim 6369

This theorem is used by:  limuni2  6428  limuni3  7854  tfinds2  7866  dfom2  7870  limomss  7873  nnlim  7882  limom  7884  ssnlim  7888  onfununi  8334  tfr1a  8387  tz7.44lem1  8398  tz7.44-2  8400  tz7.44-3  8401  1ellim  8489  2ellim  8490  oeeulem  8593  limensuc  9149  elom3  9624  r1funlim  9745  rankxplim2  9859  rankxplim3  9860  rankxpsuc  9861  infxpenlem  10013  alephislim  10083  cflim2  10262  winalim  10695  rankcf  10777  gruina  10818  cutbdaybnd2lim  28041  rdgprc0  36320  dfrdg2  36322  dfrdg4  36480  limsucncmpi  37013  limsucncmp  37014  omlimcl2  44027  onexlimgt  44028  onov0suclim  44059  succlg  44113  dflim5  44114  nlim1NEW  44226  nlim2NEW  44227  nlim3  44228  nlim4  44229  dfsucon  44307