Theorem ordeq 6355

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1562  Tr wtr 5209   E cep 5548   We wwe 5601  Ord word 6347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-v 3458  df-ss 3923  df-uni 4868  df-tr 5210  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-ord 6351

This theorem is referenced by:  elong  6356  limeq  6360  ordelord  6370  ordun  6454  ordeleqon  7767  ordsuc  7796  ordzsl  7827  issmo  8321  issmo2  8322  smoeq  8323  smores  8325  smores2  8327  smodm2  8328  smoiso  8335  tfrlem8  8357  ord3  8455  ordtypelem5  9472  ordtypelem7  9474  oicl  9479  oieu  9489  fineqvnttrclse  35424  dfsucon  44104