Theorem equsexvw 2037

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 2036. (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 1875	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
2		equsalvw.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	notbid 321	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
4	3	equsalvw 2036	. . 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 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999

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

This theorem is used by:  equvinv  2061  cleljust  2153  sbelx  2288  cleljustab  2741  axsepgfromrep  5246  dfid3  5548  opeliunxp  5717  opeliun2xp  5718  imai  6071  coi1  6264  opabex3d  7977  opabex3rd  7978  opabex3  7979  fsplit  8128  mapsnend  9064  elirrv  9591  elirrvOLD  9592  dfac5lem1  10202  dfac5lem3  10204  dffix2  36709  sscoid  36717  elfuns  36719  negprop  38686  pmapglb  40870  polval2N  41006  tfsconcat0i  44390