Theorem limeq 6397

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086   = wceq 1536   ≠ wne 2937  ∅c0 4338  ∪ cuni 4911  Ord word 6384  Lim wlim 6386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-v 3479  df-ss 3979  df-uni 4912  df-tr 5265  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-lim 6390

This theorem is referenced by:  limuni2  6447  0ellim  6448  limuni3  7872  tfinds2  7884  dfom2  7888  limomss  7891  nnlim  7900  limom  7902  ssnlim  7906  onfununi  8379  tfr1a  8432  tz7.44lem1  8443  tz7.44-2  8445  tz7.44-3  8446  1ellim  8534  2ellim  8535  oeeulem  8637  limensuc  9192  elom3  9685  r1funlim  9803  rankxplim2  9917  rankxplim3  9918  rankxpsuc  9919  infxpenlem  10050  alephislim  10120  cflim2  10300  winalim  10732  rankcf  10814  gruina  10855  scutbdaybnd2lim  27876  rdgprc0  35774  dfrdg2  35776  dfrdg4  35932  limsucncmpi  36427  limsucncmp  36428  omlimcl2  43230  onexlimgt  43231  onov0suclim  43263  succlg  43317  dflim5  43318  nlim1NEW  43431  nlim2NEW  43432  nlim3  43433  nlim4  43434  dfsucon  43512