Theorem weeq12d 5645

Description: Equality deduction for well-orderings. (Contributed by Stefan O'Rear, 19-Jan-2015.) (Proof shortened by Matthew House, 10-Sep-2025.)

Hypotheses

Ref	Expression
weeq12d.1	⊢ (𝜑 → 𝑅 = 𝑆)
weeq12d.2	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
weeq12d	⊢ (𝜑 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐵))

Proof of Theorem weeq12d

Step	Hyp	Ref	Expression
1		weeq12d.1	. 2 ⊢ (𝜑 → 𝑅 = 𝑆)
2		weeq12d.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		weeq1 5643	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴))
4		weeq2 5644	. . 3 ⊢ (𝐴 = 𝐵 → (𝑆 We 𝐴 ↔ 𝑆 We 𝐵))
5	3, 4	sylan9bb 519	. 2 ⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → (𝑅 We 𝐴 ↔ 𝑆 We 𝐵))
6	1, 2, 5	syl2anc 596	1 ⊢ (𝜑 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   We wwe 5608

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-ex 1813  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-ss 3901  df-br 5107  df-po 5564  df-so 5565  df-fr 5609  df-we 5611

This theorem is used by:  fnwe2lem2  8176  hartogslem1  9566  fpwwe2cbv  10745  fpwwe2lem2  10747  fpwwe2lem4  10749  fpwwecbv  10759  fpwwelem  10760  canthwelem  10765  canthwe  10766  pwfseqlem4  10777  werankwe  35834  werankwe2  35835  acwer1prclem  35864  onprcf1acwevdlem2  36059  onf1oracwevd  36065  aomclem1  44260  aomclem4  44263  aomclem5  44264  aomclem6  44265