Theorem limeq 6171

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 6166	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 3049	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4811	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2814	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1433	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6164	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6164	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1084   = wceq 1538   ≠ wne 2987  ∅c0 4243  ∪ cuni 4800  Ord word 6158  Lim wlim 6160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-ral 3111  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-tr 5137  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-ord 6162  df-lim 6164

This theorem is referenced by:  limuni2  6220  0ellim  6221  limuni3  7547  tfinds2  7558  dfom2  7562  limomss  7565  nnlim  7573  limom  7575  ssnlim  7579  onfununi  7961  tfr1a  8013  tz7.44lem1  8024  tz7.44-2  8026  tz7.44-3  8027  oeeulem  8210  limensuc  8678  elom3  9095  r1funlim  9179  rankxplim2  9293  rankxplim3  9294  rankxpsuc  9295  infxpenlem  9424  alephislim  9494  cflim2  9674  winalim  10106  rankcf  10188  gruina  10229  rdgprc0  33151  dfrdg2  33153  dfrdg4  33525  limsucncmpi  33906  limsucncmp  33907  dfsucon  40231