Theorem limeq 6358

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 6353	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 3019	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4876	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2778	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1457	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6351	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6351	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1098   = wceq 1560   ≠ wne 2957  ∅c0 4285  ∪ cuni 4865  Ord word 6345  Lim wlim 6347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1100  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-v 3456  df-ss 3921  df-uni 4866  df-tr 5208  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-ord 6349  df-lim 6351

This theorem is referenced by:  limuni2  6409  limuni3  7832  tfinds2  7844  dfom2  7848  limomss  7851  nnlim  7860  limom  7862  ssnlim  7866  onfununi  8312  tfr1a  8365  tz7.44lem1  8376  tz7.44-2  8378  tz7.44-3  8379  1ellim  8467  2ellim  8468  oeeulem  8571  limensuc  9126  elom3  9603  r1funlim  9724  rankxplim2  9838  rankxplim3  9839  rankxpsuc  9840  infxpenlem  9969  alephislim  10039  cflim2  10220  winalim  10653  rankcf  10735  gruina  10776  cutbdaybnd2lim  27890  rdgprc0  36141  dfrdg2  36143  dfrdg4  36301  limsucncmpi  36805  limsucncmp  36806  omlimcl2  43819  onexlimgt  43820  onov0suclim  43851  succlg  43905  dflim5  43906  nlim1NEW  44018  nlim2NEW  44019  nlim3  44020  nlim4  44021  dfsucon  44099