Theorem equsalvw 2034

Description: Version of equsalv 2303 with a disjoint variable condition, and of equsal 2449 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw 2035. (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 1849	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜓))
4		equsv 2033	. 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 1825  ax-4 1839  ax-5 1940  ax-6 1997

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

This theorem is used by:  equsexvw  2035  equvelv  2061  sb6  2119  sbievwOLD  2129  ax13lem2  2408  reu8  3696  elOLD  5420  asymref2  6117  intirr  6118  fun11  6610  fv3  6899  elirrvOLD  9556  fpwwe2lem11  10630  axprALT2  35512  axreg  35548  axregscl  35549  mh-prprimbi  37082  bj-dvelimdv  37514  bj-dvelimdv1  37515  undmrnresiss  44358  pm13.192  45148