Theorem equsexvw 2038

Description: Version of equsexv 2302 with a disjoint variable condition, and of equsex 2447 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2037. (Contributed by BJ, 31-May-2019.) (Proof shortened by Wolf Lammen, 23-Oct-2023.)

Hypothesis

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

Assertion

Ref	Expression
equsexvw	⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)

Distinct variable groups:   𝑥,𝑦   𝜓,𝑥

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

Proof of Theorem equsexvw

Step	Hyp	Ref	Expression
1		alinexa 1876	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
2		equsalvw.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	notbid 321	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
4	3	equsalvw 2037	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ 𝜓)
5	1, 4	bitr3i 280	. 2 ⊢ (¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ¬ 𝜓)
6	5	con4bii 324	1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812

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 1943  ax-6 2000

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

This theorem is used by:  equvinv  2062  cleljust  2154  sbelx  2288  cleljustab  2741  axsepgfromrep  5246  dfid3  5545  opeliunxp  5714  opeliun2xp  5715  imai  6064  coi1  6253  opabex3d  7960  opabex3rd  7961  opabex3  7962  fsplit  8111  mapsnend  9042  elirrv  9569  elirrvOLD  9570  dfac5lem1  10173  dfac5lem3  10175  dffix2  36589  sscoid  36597  elfuns  36599  negprop  38563  pmapglb  40747  polval2N  40883  tfsconcat0i  44290