Theorem limeq 6322

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 6317	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 2996	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4849	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2755	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1444	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6315	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6315	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 315	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1092   = wceq 1547   ≠ wne 2934  ∅c0 4261  ∪ cuni 4838  Ord word 6309  Lim wlim 6311

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-v 3433  df-ss 3900  df-uni 4839  df-tr 5180  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-ord 6313  df-lim 6315

This theorem is referenced by:  limuni2  6373  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  9082  elom3  9560  r1funlim  9681  rankxplim2  9795  rankxplim3  9796  rankxpsuc  9797  infxpenlem  9926  alephislim  9996  cflim2  10176  winalim  10609  rankcf  10691  gruina  10732  cutbdaybnd2lim  27807  rdgprc0  36019  dfrdg2  36021  dfrdg4  36179  limsucncmpi  36673  limsucncmp  36674  omlimcl2  43687  onexlimgt  43688  onov0suclim  43719  succlg  43773  dflim5  43774  nlim1NEW  43886  nlim2NEW  43887  nlim3  43888  nlim4  43889  dfsucon  43967