Theorem limeq 6337

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 6332	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 2995	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4876	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2753	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1439	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6330	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6330	. 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 4287  ∪ cuni 4865  Ord word 6324  Lim wlim 6326

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 3444  df-ss 3920  df-uni 4866  df-tr 5208  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-lim 6330

This theorem is referenced by:  limuni2  6388  limuni3  7804  tfinds2  7816  dfom2  7820  limomss  7823  nnlim  7832  limom  7834  ssnlim  7838  onfununi  8283  tfr1a  8335  tz7.44lem1  8346  tz7.44-2  8348  tz7.44-3  8349  1ellim  8435  2ellim  8436  oeeulem  8539  limensuc  9094  elom3  9569  r1funlim  9690  rankxplim2  9804  rankxplim3  9805  rankxpsuc  9806  infxpenlem  9935  alephislim  10005  cflim2  10185  winalim  10618  rankcf  10700  gruina  10741  cutbdaybnd2lim  27805  rdgprc0  36007  dfrdg2  36009  dfrdg4  36167  limsucncmpi  36661  limsucncmp  36662  omlimcl2  43599  onexlimgt  43600  onov0suclim  43631  succlg  43685  dflim5  43686  nlim1NEW  43798  nlim2NEW  43799  nlim3  43800  nlim4  43801  dfsucon  43879