Theorem limeq 6364

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 6359	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 2994	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4894	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2751	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1438	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6357	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6357	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086   = wceq 1540   ≠ wne 2932  ∅c0 4308  ∪ cuni 4883  Ord word 6351  Lim wlim 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-v 3461  df-ss 3943  df-uni 4884  df-tr 5230  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-ord 6355  df-lim 6357

This theorem is referenced by:  limuni2  6415  0ellim  6416  limuni3  7845  tfinds2  7857  dfom2  7861  limomss  7864  nnlim  7873  limom  7875  ssnlim  7879  onfununi  8353  tfr1a  8406  tz7.44lem1  8417  tz7.44-2  8419  tz7.44-3  8420  1ellim  8508  2ellim  8509  oeeulem  8611  limensuc  9166  elom3  9660  r1funlim  9778  rankxplim2  9892  rankxplim3  9893  rankxpsuc  9894  infxpenlem  10025  alephislim  10095  cflim2  10275  winalim  10707  rankcf  10789  gruina  10830  scutbdaybnd2lim  27779  rdgprc0  35757  dfrdg2  35759  dfrdg4  35915  limsucncmpi  36409  limsucncmp  36410  omlimcl2  43213  onexlimgt  43214  onov0suclim  43245  succlg  43299  dflim5  43300  nlim1NEW  43413  nlim2NEW  43414  nlim3  43415  nlim4  43416  dfsucon  43494