Theorem equsexvw 2040

Description: Version of equsexv 2306 with a disjoint variable condition, and of equsex 2450 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2039. (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 2039	. . 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 1945  ax-6 2002

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

This theorem is used by:  equvinv  2064  cleljust  2156  sbelx  2292  cleljustab  2744  axsepgfromrep  5250  dfid3  5553  opeliunxp  5722  opeliun2xp  5723  imai  6084  coi1  6279  opabex3d  8001  opabex3rd  8002  opabex3  8003  fsplit  8155  mapsnend  9092  elirrv  9618  elirrvOLD  9619  dfac5lem1  10229  dfac5lem3  10231  dffix2  36845  sscoid  36853  elfuns  36855  coi1res  38151  negprop  38835  pmapglb  41019  polval2N  41155  tfsconcat0i  44539