Theorem equsalvw 2039

Description: Version of equsalv 2305 with a disjoint variable condition, and of equsal 2449 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw 2040. (Contributed by BJ, 31-May-2019.)

Hypothesis

Ref	Expression
equsalvw.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
equsalvw	⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)

Distinct variable groups:   𝑥,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝜓(𝑦)

Proof of Theorem equsalvw

Step	Hyp	Ref	Expression
1		equsalvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	pm5.74i 274	. . 3 ⊢ ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜓))
3	2	albii 1852	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜓))
4		equsv 2038	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜓)
5	3, 4	bitri 278	1 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568

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

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  equsexvw  2040  equvelv  2066  sb6  2124  ax13lem2  2408  reu8  3694  el.OLD  5411  asymref2  6122  intirr  6123  fun11  6633  fv3  6923  elirrvOLD  9616  fpwwe2lem11  10750  axprALT2  35815  axreg  35894  axregscl  35895  mh-prprimbi  37508  bj-dvelimdv  37940  bj-dvelimdv1  37941  undmrnresiss  44794  pm13.192  45584