Theorem limeq 6275

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 6270	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 3007	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4855	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2755	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1434	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6268	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6268	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 313	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085   = wceq 1541   ≠ wne 2944  ∅c0 4261  ∪ cuni 4844  Ord word 6262  Lim wlim 6264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-v 3432  df-in 3898  df-ss 3908  df-uni 4845  df-tr 5196  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-ord 6266  df-lim 6268

This theorem is referenced by:  limuni2  6324  0ellim  6325  limuni3  7687  tfinds2  7698  dfom2  7702  limomss  7705  nnlim  7714  limom  7716  ssnlim  7720  onfununi  8156  tfr1a  8209  tz7.44lem1  8220  tz7.44-2  8222  tz7.44-3  8223  oeeulem  8408  limensuc  8906  elom3  9367  r1funlim  9508  rankxplim2  9622  rankxplim3  9623  rankxpsuc  9624  infxpenlem  9753  alephislim  9823  cflim2  10003  winalim  10435  rankcf  10517  gruina  10558  rdgprc0  33748  dfrdg2  33750  scutbdaybnd2lim  33990  dfrdg4  34232  limsucncmpi  34613  limsucncmp  34614  dfsucon  41092