Theorem ordeq 6369

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 5218	. . 3 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
2		weeq2 5638	. . 3 ⊢ (𝐴 = 𝐵 → ( E We 𝐴 ↔ E We 𝐵))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐴 = 𝐵 → ((Tr 𝐴 ∧ E We 𝐴) ↔ (Tr 𝐵 ∧ E We 𝐵)))
4		df-ord 6365	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
5		df-ord 6365	. 2 ⊢ (Ord 𝐵 ↔ (Tr 𝐵 ∧ E We 𝐵))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  Tr wtr 5211   E cep 5549   We wwe 5602  Ord word 6361

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3896  df-uni 4867  df-tr 5212  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365

This theorem is used by:  elong  6370  limeq  6374  ordelord  6384  ordun  6469  ordeleqon  7796  ordsuc  7825  ordzsl  7856  issmo  8356  issmo2  8357  smoeq  8358  smores  8360  smores2  8362  smodm2  8363  smoiso  8370  tfrlem8  8392  ord3  8492  ordtypelem5  9516  ordtypelem7  9518  oicl  9523  oieu  9533  fineqvnttrclse  35792  dfsucon  44524