Theorem limeq 6327

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 6322	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 2992	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4872	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2750	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1438	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6320	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6320	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086   = wceq 1541   ≠ wne 2930  ∅c0 4283  ∪ cuni 4861  Ord word 6314  Lim wlim 6316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-v 3440  df-ss 3916  df-uni 4862  df-tr 5204  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-lim 6320

This theorem is referenced by:  limuni2  6378  limuni3  7792  tfinds2  7804  dfom2  7808  limomss  7811  nnlim  7820  limom  7822  ssnlim  7826  onfununi  8271  tfr1a  8323  tz7.44lem1  8334  tz7.44-2  8336  tz7.44-3  8337  1ellim  8423  2ellim  8424  oeeulem  8527  limensuc  9080  elom3  9555  r1funlim  9676  rankxplim2  9790  rankxplim3  9791  rankxpsuc  9792  infxpenlem  9921  alephislim  9991  cflim2  10171  winalim  10604  rankcf  10686  gruina  10727  scutbdaybnd2lim  27785  rdgprc0  35934  dfrdg2  35936  dfrdg4  36094  limsucncmpi  36588  limsucncmp  36589  omlimcl2  43426  onexlimgt  43427  onov0suclim  43458  succlg  43512  dflim5  43513  nlim1NEW  43625  nlim2NEW  43626  nlim3  43627  nlim4  43628  dfsucon  43706