Theorem limeq 6330

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 6325	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 2995	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4862	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2753	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1439	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6323	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6323	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087   = wceq 1542   ≠ wne 2933  ∅c0 4274  ∪ cuni 4851  Ord word 6317  Lim wlim 6319

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-v 3432  df-ss 3907  df-uni 4852  df-tr 5194  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6321  df-lim 6323

This theorem is referenced by:  limuni2  6381  limuni3  7797  tfinds2  7809  dfom2  7813  limomss  7816  nnlim  7825  limom  7827  ssnlim  7831  onfununi  8275  tfr1a  8327  tz7.44lem1  8338  tz7.44-2  8340  tz7.44-3  8341  1ellim  8427  2ellim  8428  oeeulem  8531  limensuc  9086  elom3  9563  r1funlim  9684  rankxplim2  9798  rankxplim3  9799  rankxpsuc  9800  infxpenlem  9929  alephislim  9999  cflim2  10179  winalim  10612  rankcf  10694  gruina  10735  cutbdaybnd2lim  27806  rdgprc0  35992  dfrdg2  35994  dfrdg4  36152  limsucncmpi  36646  limsucncmp  36647  omlimcl2  43691  onexlimgt  43692  onov0suclim  43723  succlg  43777  dflim5  43778  nlim1NEW  43890  nlim2NEW  43891  nlim3  43892  nlim4  43893  dfsucon  43971