Theorem ordeq 6321

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 5189	. . 3 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
2		weeq2 5609	. . 3 ⊢ (𝐴 = 𝐵 → ( E We 𝐴 ↔ E We 𝐵))
3	1, 2	anbi12d 639	. 2 ⊢ (𝐴 = 𝐵 → ((Tr 𝐴 ∧ E We 𝐴) ↔ (Tr 𝐵 ∧ E We 𝐵)))
4		df-ord 6317	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
5		df-ord 6317	. 2 ⊢ (Ord 𝐵 ↔ (Tr 𝐵 ∧ E We 𝐵))
6	3, 4, 5	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548  Tr wtr 5182   E cep 5520   We wwe 5573  Ord word 6313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-v 3435  df-ss 3902  df-uni 4842  df-tr 5183  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317

This theorem is referenced by:  elong  6322  limeq  6326  ordelord  6336  ordun  6420  ordeleqon  7729  ordsuc  7758  ordzsl  7789  issmo  8282  issmo2  8283  smoeq  8284  smores  8286  smores2  8288  smodm2  8289  smoiso  8296  tfrlem8  8317  ord3  8414  ordtypelem5  9431  ordtypelem7  9433  oicl  9438  oieu  9448  fineqvnttrclse  35320  dfsucon  43982