Theorem equsalvw 2026

Description: Version of equsalv 2304 with a disjoint variable condition, and of equsal 2450 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw 2027. (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 273	. . 3 ⊢ ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜓))
3	2	albii 1841	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜓))
4		equsv 2025	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜓)
5	3, 4	bitri 277	1 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989

This theorem depends on definitions:  df-bi 209  df-ex 1802

This theorem is referenced by:  equsexvw  2027  equvelv  2053  sb6  2120  sbievwOLD  2130  ax13lem2  2409  reu8  3698  elOLD  5408  asymref2  6106  intirr  6107  fun11  6597  fv3  6887  elirrvOLD  9548  fpwwe2lem11  10601  axprALT2  35409  axreg  35427  axregscl  35428  mh-prprimbi  36908  bj-dvelimdv  37341  bj-dvelimdv1  37342  undmrnresiss  44185  pm13.192  44991