Theorem weeq12d 5639

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 5637	. . 3 ⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴))
4		weeq2 5638	. . 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 1569   We wwe 5602

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-or 862  df-3or 1104  df-ex 1812  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-ss 3896  df-br 5103  df-po 5558  df-so 5559  df-fr 5603  df-we 5605

This theorem is used by:  fnwe2lem2  8148  hartogslem1  9539  fpwwe2cbv  10718  fpwwe2lem2  10720  fpwwe2lem4  10722  fpwwecbv  10732  fpwwelem  10733  canthwelem  10738  canthwe  10739  pwfseqlem4  10750  werankwe  35791  werankwe2  35792  acwer1prclem  35815  onprcf1acwevdlem2  35965  onf1oracwevd  35971  aomclem1  44149  aomclem4  44152  aomclem5  44153  aomclem6  44154