Theorem ordeq 6314

Description: Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)

Assertion

Ref	Expression
ordeq	⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))

Proof of Theorem ordeq

Step	Hyp	Ref	Expression
1		treq 5206	. . 3 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
2		weeq2 5607	. . 3 ⊢ (𝐴 = 𝐵 → ( E We 𝐴 ↔ E We 𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((Tr 𝐴 ∧ E We 𝐴) ↔ (Tr 𝐵 ∧ E We 𝐵)))
4		df-ord 6310	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
5		df-ord 6310	. 2 ⊢ (Ord 𝐵 ↔ (Tr 𝐵 ∧ E We 𝐵))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  Tr wtr 5199   E cep 5518   We wwe 5571  Ord word 6306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3438  df-ss 3920  df-uni 4859  df-tr 5200  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6310

This theorem is referenced by:  elong  6315  limeq  6319  ordelord  6329  ordun  6413  ordeleqon  7718  ordsuc  7747  ordzsl  7778  issmo  8271  issmo2  8272  smoeq  8273  smores  8275  smores2  8277  smodm2  8278  smoiso  8285  tfrlem8  8306  ord3  8403  ordtypelem5  9414  ordtypelem7  9416  oicl  9421  oieu  9431  fineqvnttrclse  35083  dfsucon  43506