Theorem ordeq 6368

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 5223	. . 3 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
2		weeq2 5647	. . 3 ⊢ (𝐴 = 𝐵 → ( E We 𝐴 ↔ E We 𝐵))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐴 = 𝐵 → ((Tr 𝐴 ∧ E We 𝐴) ↔ (Tr 𝐵 ∧ E We 𝐵)))
4		df-ord 6364	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
5		df-ord 6364	. 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 1570  Tr wtr 5216   E cep 5558   We wwe 5611  Ord word 6360

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-v 3455  df-ss 3919  df-uni 4871  df-tr 5217  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364

This theorem is used by:  elong  6369  limeq  6373  ordelord  6383  ordun  6468  ordeleqon  7784  ordsuc  7813  ordzsl  7844  issmo  8340  issmo2  8341  smoeq  8342  smores  8344  smores2  8346  smodm2  8347  smoiso  8354  tfrlem8  8376  ord3  8474  ordtypelem5  9497  ordtypelem7  9499  oicl  9504  oieu  9514  fineqvnttrclse  35637  dfsucon  44350