Theorem equsalvw 2012

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975

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

This theorem is referenced by:  equsexvw  2013  equvelv  2039  sb6  2097  sbievwOLD  2107  ax13lem2  2386  reu8  3676  elOLD  5381  asymref2  6074  intirr  6075  fun11  6563  fv3  6849  elirrvOLD  9507  fpwwe2lem11  10559  axprALT2  35305  axreg  35323  axregscl  35324  mh-prprimbi  36786  bj-dvelimdv  37219  bj-dvelimdv1  37220  undmrnresiss  44063  pm13.192  44869